A hybrid formal verification approach for QoS-aware multi-cloud service composition
Tóm tắt
Today, cloud providers represent their individual services with several functional and non-functional properties in various environments. Discovering and selecting an appropriate atomic service from a pool of activated services are a main challenge in the multi-cloud service composition. Minimizing the number of cloud providers is a critical matter in the service composition problem, which effects on energy consumption, response time and total cost. This paper presents a hybrid formal verification approach to assess the service composition in multi-cloud environments though the decreasing number of cloud providers to gain final service composition with a high level of Quality of Service (QoS). The presented approach provides behavioral modeling to examine the procedure of user’ requests, service selection, and composition in a multi-cloud environment. Also, the proposed approach permits analysis of the service composition using a Multi-Labeled Transition Systems (MLTS)-based model checking and Pi-Calculus-based process algebra methods for monitoring the functional specifications and non-functional properties as the QoS standards. In addition, the proposed approach satisfies the functional properties for the multi-cloud service composition. The experimental results proved the feasibility of the proposed approach with performance evaluations and some confirmation setups.
Tài liệu tham khảo
Maamar, Z., et al.: Towards a seamless coordination of cloud and fog: illustration through the internet-of-things. In Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, pp. 2008–2015. ACM, Limassol, Cyprus (2019)
Shojafar, M., et al.: Recent advances in cloud data centers toward fog data centers. Concurr. Comput. 31(8), e5164 (2019)
Buyya, R., Broberg, J., Goscinski, A.M.: Cloud Computing: Principles and Paradigms, vol. 87. Wiley, Hoboken (2010)
Tajiki, M.M., et al.: CECT: computationally efficient congestion-avoidance and traffic engineering in software-defined cloud data centers. Clust. Comput. 21(4), 1881–1897 (2018)
Aceto, G., et al.: Cloud monitoring: a survey. Comput. Netw. 57(9), 2093–2115 (2013)
Stergiou, C., et al.: Secure integration of IoT and cloud computing. Future Gener. Comput. Syst. 78, 964–975 (2018)
Ghobaei-Arani, M., Souri, A.: LP-WSC: a linear programming approach for web service composition in geographically distributed cloud environments. J. Supercomput. 75(5), 2603–2628 (2019)
Simon, B., Goldschmidt, B., Kondorosi, K.: A metamodel for the web services standards. J. Grid Comput. 11(4), 735–752 (2013)
Piprani, B., Sheppard, D., Barbir, A.: Comparative analysis of SOA and cloud computing architectures using fact based modeling. In: Proceedings of the OTM Confederated International Conferences on the Move to Meaningful Internet Systems. Springer (2013)
Portchelvi, V., Venkatesan, V.P., Shanmugasundaram, G.: Achieving web services composition–a survey. Softw. Eng. 2(5), 195–202 (2012)
Brahmi, Z., Faten, M.: Service composition in a multi-cloud environment based on cooperative agents
Barkat, A., Okba, K., Bourekkache, S.: Service composition in the multi cloud environment. Int. J. Web Inf. Syst. 13(4), 471–484 (2017)
Keshanchi, B., Souri, A., Navimipour, N.J.: An improved genetic algorithm for task scheduling in the cloud environments using the priority queues: formal verification, simulation, and statistical testing. J. Syst. Softw. 124, 1–21 (2017)
Naseri, A., Navimipour, N.J.: A new agent-based method for QoS-aware cloud service composition using particle swarm optimization algorithm. J. Ambient Intell. Hum. Comput. 10, 1851–1864 (2018)
Ghobaei-Arani, M., et al.: CSA-WSC: cuckoo search algorithm for web service composition in cloud environments. Soft Comput. 22, 8353–8378 (2017)
Imran, M., et al.: Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications. Wireless Netw. 22(1), 247–265 (2016)
Dumez, C., et al.: Model-driven approach supporting formal verification for web service composition protocols. J. Netw. Comput. Appl. 36(4), 1102–1115 (2013)
Diekmann, C., et al.: Verified iptables firewall analysis and verification. J. Autom. Reason. 61(1), 191–242 (2018)
Ghobaei-Arani, M., et al.: A moth-flame optimization algorithm for web service composition in cloud computing: simulation and verification. Software 48(10), 1865–1892 (2018)
Souri, A., Rahmani, A.M., Jafari Navimipour, N.: Formal verification approaches in the web service composition: a comprehensive analysis of the current challenges for future research. Int. J. Commun. Syst. 31(17), 3808 (2018)
Souri, A., Navimipour, N.J., Rahmani, A.M.: Formal verification approaches and standards in the cloud computing: a comprehensive and systematic review. Comput. Stand. Interfaces 58, 1–22 (2018)
Amato, F., Moscato, F.: Model transformations of MapReduce Design Patterns for automatic development and verification. J. Parallel Distrib. Comput. 110, 52–59 (2017)
Souria, A., Shariflooa, M.A., Norouzia, M.: Analyzing SMV & UPPAAL model checkers in real-time systems. Comput. Sci. 1, 631–639 (2012)
Frenkel, H., Grumberg, O., Sheinvald, S.: An automata-theoretic approach to model-checking systems and specifications over infinite data domains. J. Autom. eason. 63, 1077–1101 (2018)
Yu, B., et al.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89–99 (2018)
Gao, H., et al.: Research on cost-driven services composition in an uncertain environment. J. Internet Technol.y 20(3), 755–769 (2019)
Li, Y., Yao, X.: Cloud manufacturing service composition and formal verification based on extended process calculus. Adv. Mech. Eng. (2018). https://doi.org/10.1177/1687814018781287
Bourne, S., Szabo, C., Sheng, Q.Z.: Transactional behavior verification in business process as a service configuration. IEEE Trans. Serv. Comput. 12(2), 290–303 (2019)
Souri, A., et al.: Formal modeling and verification of a service composition approach in the social customer relationship management system. Inf. Technol. People (2019). https://doi.org/10.1108/ITP-02-2018-0109
Ghobaei-Arani, M., et al.: A moth-flame optimization algorithm for web service composition in cloud computing: simulation and verification. Software 48, 1865–1892 (2018)
Mezni, H., Sellami, M.: Multi-cloud service composition using formal concept analysis. J. Syst. Softw. 134, 138–152 (2017)
Entezari-Maleki, R., et al.: Modeling and evaluation of service composition in commercial multiclouds using timed colored petri nets. In: IEEE Transactions on Systems, Man, and Cybernetics: Systems. pp. 1–15 (2017)
Rai, G.N., et al.: Web service interaction modeling and verification using recursive composition algebra. IEEE Transactions on Services Computing. pp. 1–1 (2018)
Khai, H.T., Thang, B.H., Tho, Q.T.: One size does not fit all: logic-based clustering for on-the-fly web service composition and verification. Int. J. Web Grid Serv. 14(3), 237–272 (2018)
Saeed, S., et al.: A location-sensitive and network-aware broker for recommending Web services. Computing 101(5), 455–475 (2019)
Wang, H., et al.: Integrating modified cuckoo algorithm and creditability evaluation for QoS-aware service composition. Knowl. Based Syst. 140, 64–81 (2018)
Souri, A., et al.: A symbolic model checking approach in formal verification of distributed systems. Human Centric Comput. Inf. Sci. 9(1), 4 (2019)
Gyftopoulos, S., Efraimidis, P.S., Katsaros, P.: Formal analysis of DeGroot Influence Problems using probabilistic model checking. Simul. Model. Pract. Theory 89, 144–159 (2018)
Arapinis, M., et al.: Statverif: verification of stateful processes. Journal of Computer Security 22(5), 743–821 (2014)
Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: International Conference on Foundations of Software Science and Computation Structures. Springer (2018)
Ryan, M.D., Smyth, B.: Applied pi calculus. J ACM 65, 1 (2011)
Rodriguez-Mier, P., et al.: An integrated semantic web service discovery and composition framework. IEEE Trans. Serv. Comput. 9(4), 537–550 (2016)
Souri, A., Jafari Navimipour, N.: Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Syst. Appl. 41(8), 3831–3849 (2014)
Souri, A., et al.: A model checking approach for user relationship management in the social network. Kybernetes 48(3), 407–423 (2019)
Zhao, X., et al.: An improved discrete immune optimization algorithm based on PSO for QoS-driven web service composition. Appl. Soft Comput. 12(8), 2208–2216 (2012)
Mardukhi, F., et al.: QoS decomposition for service composition using genetic algorithm. Appl. Soft Comput. 13(7), 3409–3421 (2013)
Entezari-Maleki, R., et al.: Modeling and Evaluation of Service Composition in Commercial Multiclouds Using Timed Colored Petri Nets. In: IEEE Transactions on Systems, Man, and Cybernetics: Systems (2017)
Arunkumar, G., Venkataraman, N.: A novel approach to address interoperability concern in cloud computing. Proc. Comput. Sci. 50, 554–559 (2015)
Rezaei, R., et al.: A semantic interoperability framework for software as a service systems in cloud computing environments. Expert Syst. Appl. 41(13), 5751–5770 (2014)
Fatma, L., Haithem, M.: Multicloud service composition: a survey of current approaches and issues. J. Softw. 30(10), e1947 (2018)