{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T13:13:24Z","timestamp":1771679604998,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T00:00:00Z","timestamp":1574899200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T00:00:00Z","timestamp":1574899200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10586-019-03018-9","type":"journal-article","created":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T05:34:13Z","timestamp":1574919253000},"page":"2453-2470","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":66,"title":["A hybrid formal verification approach for QoS-aware multi-cloud service composition"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8314-9051","authenticated-orcid":false,"given":"Alireza","family":"Souri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir Masoud","family":"Rahmani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nima Jafari","family":"Navimipour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reza","family":"Rezaei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,28]]},"reference":[{"key":"3018_CR1","doi-asserted-by":"crossref","unstructured":"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\u20132015. ACM, Limassol, Cyprus (2019)","DOI":"10.1145\/3297280.3297477"},{"issue":"8","key":"3018_CR2","doi-asserted-by":"crossref","first-page":"e5164","DOI":"10.1002\/cpe.5164","volume":"31","author":"M Shojafar","year":"2019","unstructured":"Shojafar, M., et al.: Recent advances in cloud data centers toward fog data centers. Concurr. Comput. 31(8), e5164 (2019)","journal-title":"Concurr. Comput."},{"key":"3018_CR3","volume-title":"Cloud Computing: Principles and Paradigms","author":"R Buyya","year":"2010","unstructured":"Buyya, R., Broberg, J., Goscinski, A.M.: Cloud Computing: Principles and Paradigms, vol. 87. Wiley, Hoboken (2010)"},{"issue":"4","key":"3018_CR4","doi-asserted-by":"crossref","first-page":"1881","DOI":"10.1007\/s10586-018-2815-6","volume":"21","author":"MM Tajiki","year":"2018","unstructured":"Tajiki, M.M., et al.: CECT: computationally efficient congestion-avoidance and traffic engineering in software-defined cloud data centers. Clust. Comput. 21(4), 1881\u20131897 (2018)","journal-title":"Clust. Comput."},{"issue":"9","key":"3018_CR5","doi-asserted-by":"crossref","first-page":"2093","DOI":"10.1016\/j.comnet.2013.04.001","volume":"57","author":"G Aceto","year":"2013","unstructured":"Aceto, G., et al.: Cloud monitoring: a survey. Comput. Netw. 57(9), 2093\u20132115 (2013)","journal-title":"Comput. Netw."},{"key":"3018_CR6","doi-asserted-by":"crossref","first-page":"964","DOI":"10.1016\/j.future.2016.11.031","volume":"78","author":"C Stergiou","year":"2018","unstructured":"Stergiou, C., et al.: Secure integration of IoT and cloud computing. Future Gener. Comput. Syst. 78, 964\u2013975 (2018)","journal-title":"Future Gener. Comput. Syst."},{"issue":"5","key":"3018_CR7","doi-asserted-by":"crossref","first-page":"2603","DOI":"10.1007\/s11227-018-2656-3","volume":"75","author":"M Ghobaei-Arani","year":"2019","unstructured":"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\u20132628 (2019)","journal-title":"J. Supercomput."},{"issue":"4","key":"3018_CR8","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1007\/s10723-013-9273-4","volume":"11","author":"B Simon","year":"2013","unstructured":"Simon, B., Goldschmidt, B., Kondorosi, K.: A metamodel for the web services standards. J. Grid Comput. 11(4), 735\u2013752 (2013)","journal-title":"J. Grid Comput."},{"key":"3018_CR9","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-642-41033-8_66"},{"issue":"5","key":"3018_CR10","first-page":"195","volume":"2","author":"V Portchelvi","year":"2012","unstructured":"Portchelvi, V., Venkatesan, V.P., Shanmugasundaram, G.: Achieving web services composition\u2013a survey. Softw. Eng. 2(5), 195\u2013202 (2012)","journal-title":"Softw. Eng."},{"key":"3018_CR11","unstructured":"Brahmi, Z., Faten, M.: Service composition in a multi-cloud environment based on cooperative agents"},{"issue":"4","key":"3018_CR12","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1108\/IJWIS-08-2016-0047","volume":"13","author":"A Barkat","year":"2017","unstructured":"Barkat, A., Okba, K., Bourekkache, S.: Service composition in the multi cloud environment. Int. J. Web Inf. Syst. 13(4), 471\u2013484 (2017)","journal-title":"Int. J. Web Inf. Syst."},{"key":"3018_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jss.2016.07.006","volume":"124","author":"B Keshanchi","year":"2017","unstructured":"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\u201321 (2017)","journal-title":"J. Syst. Softw."},{"key":"3018_CR14","doi-asserted-by":"crossref","first-page":"1851","DOI":"10.1007\/s12652-018-0773-8","volume":"10","author":"A Naseri","year":"2018","unstructured":"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\u20131864 (2018)","journal-title":"J. Ambient Intell. Hum. Comput."},{"key":"3018_CR15","doi-asserted-by":"crossref","first-page":"8353","DOI":"10.1007\/s00500-017-2783-4","volume":"22","author":"M Ghobaei-Arani","year":"2017","unstructured":"Ghobaei-Arani, M., et al.: CSA-WSC: cuckoo search algorithm for web service composition in cloud environments. Soft Comput. 22, 8353\u20138378 (2017)","journal-title":"Soft Comput."},{"issue":"1","key":"3018_CR16","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s11276-015-0962-8","volume":"22","author":"M Imran","year":"2016","unstructured":"Imran, M., et al.: Formal verification and validation of a movement control actor relocation algorithm for safety\u2013critical applications. Wireless Netw. 22(1), 247\u2013265 (2016)","journal-title":"Wireless Netw."},{"issue":"4","key":"3018_CR17","doi-asserted-by":"crossref","first-page":"1102","DOI":"10.1016\/j.jnca.2013.01.009","volume":"36","author":"C Dumez","year":"2013","unstructured":"Dumez, C., et al.: Model-driven approach supporting formal verification for web service composition protocols. J. Netw. Comput. Appl. 36(4), 1102\u20131115 (2013)","journal-title":"J. Netw. Comput. Appl."},{"issue":"1","key":"3018_CR18","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-017-9445-1","volume":"61","author":"C Diekmann","year":"2018","unstructured":"Diekmann, C., et al.: Verified iptables firewall analysis and verification. J. Autom. Reason. 61(1), 191\u2013242 (2018)","journal-title":"J. Autom. Reason."},{"issue":"10","key":"3018_CR19","first-page":"1865","volume":"48","author":"M Ghobaei-Arani","year":"2018","unstructured":"Ghobaei-Arani, M., et al.: A moth-flame optimization algorithm for web service composition in cloud computing: simulation and verification. Software 48(10), 1865\u20131892 (2018)","journal-title":"Software"},{"issue":"17","key":"3018_CR20","doi-asserted-by":"crossref","first-page":"3808","DOI":"10.1002\/dac.3808","volume":"31","author":"A Souri","year":"2018","unstructured":"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)","journal-title":"Int. J. Commun. Syst."},{"key":"3018_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.csi.2017.11.007","volume":"58","author":"A Souri","year":"2018","unstructured":"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\u201322 (2018)","journal-title":"Comput. Stand. Interfaces"},{"key":"3018_CR22","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.jpdc.2016.12.017","volume":"110","author":"F Amato","year":"2017","unstructured":"Amato, F., Moscato, F.: Model transformations of MapReduce Design Patterns for automatic development and verification. J. Parallel Distrib. Comput. 110, 52\u201359 (2017)","journal-title":"J. Parallel Distrib. Comput."},{"key":"3018_CR23","first-page":"631","volume":"1","author":"A Souria","year":"2012","unstructured":"Souria, A., Shariflooa, M.A., Norouzia, M.: Analyzing SMV & UPPAAL model checkers in real-time systems. Comput. Sci. 1, 631\u2013639 (2012)","journal-title":"Comput. Sci."},{"key":"3018_CR24","doi-asserted-by":"crossref","first-page":"1077","DOI":"10.1007\/s10817-018-9494-0","volume":"63","author":"H Frenkel","year":"2018","unstructured":"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\u20131101 (2018)","journal-title":"J. Autom. eason."},{"key":"3018_CR25","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.jpdc.2017.09.003","volume":"118","author":"B Yu","year":"2018","unstructured":"Yu, B., et al.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89\u201399 (2018)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"3","key":"3018_CR26","first-page":"755","volume":"20","author":"H Gao","year":"2019","unstructured":"Gao, H., et al.: Research on cost-driven services composition in an uncertain environment. J. Internet Technol.y 20(3), 755\u2013769 (2019)","journal-title":"J. Internet Technol.y"},{"key":"3018_CR27","doi-asserted-by":"publisher","DOI":"10.1177\/1687814018781287","author":"Y Li","year":"2018","unstructured":"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","journal-title":"Adv. Mech. Eng."},{"issue":"2","key":"3018_CR28","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1109\/TSC.2017.2667662","volume":"12","author":"S Bourne","year":"2019","unstructured":"Bourne, S., Szabo, C., Sheng, Q.Z.: Transactional behavior verification in business process as a service configuration. IEEE Trans. Serv. Comput. 12(2), 290\u2013303 (2019)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"3018_CR29","doi-asserted-by":"publisher","DOI":"10.1108\/ITP-02-2018-0109","author":"A Souri","year":"2019","unstructured":"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","journal-title":"Inf. Technol. People"},{"key":"3018_CR30","first-page":"1865","volume":"48","author":"M Ghobaei-Arani","year":"2018","unstructured":"Ghobaei-Arani, M., et al.: A moth-flame optimization algorithm for web service composition in cloud computing: simulation and verification. Software 48, 1865\u20131892 (2018)","journal-title":"Software"},{"key":"3018_CR31","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1016\/j.jss.2017.08.016","volume":"134","author":"H Mezni","year":"2017","unstructured":"Mezni, H., Sellami, M.: Multi-cloud service composition using formal concept analysis. J. Syst. Softw. 134, 138\u2013152 (2017)","journal-title":"J. Syst. Softw."},{"key":"3018_CR32","unstructured":"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\u201315 (2017)"},{"key":"3018_CR33","doi-asserted-by":"crossref","unstructured":"Rai, G.N., et al.: Web service interaction modeling and verification using recursive composition algebra. IEEE Transactions on Services Computing. pp. 1\u20131 (2018)","DOI":"10.1109\/TSC.2018.2789454"},{"issue":"3","key":"3018_CR34","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1504\/IJWGS.2018.092579","volume":"14","author":"HT Khai","year":"2018","unstructured":"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\u2013272 (2018)","journal-title":"Int. J. Web Grid Serv."},{"issue":"5","key":"3018_CR35","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/s00607-019-00708-5","volume":"101","author":"S Saeed","year":"2019","unstructured":"Saeed, S., et al.: A location-sensitive and network-aware broker for recommending Web services. Computing 101(5), 455\u2013475 (2019)","journal-title":"Computing"},{"key":"3018_CR36","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1016\/j.knosys.2017.10.027","volume":"140","author":"H Wang","year":"2018","unstructured":"Wang, H., et al.: Integrating modified cuckoo algorithm and creditability evaluation for QoS-aware service composition. Knowl. Based Syst. 140, 64\u201381 (2018)","journal-title":"Knowl. Based Syst."},{"issue":"1","key":"3018_CR37","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1186\/s13673-019-0165-x","volume":"9","author":"A Souri","year":"2019","unstructured":"Souri, A., et al.: A symbolic model checking approach in formal verification of distributed systems. Human Centric Comput. Inf. Sci. 9(1), 4 (2019)","journal-title":"Human Centric Comput. Inf. Sci."},{"key":"3018_CR38","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/j.simpat.2018.09.009","volume":"89","author":"S Gyftopoulos","year":"2018","unstructured":"Gyftopoulos, S., Efraimidis, P.S., Katsaros, P.: Formal analysis of DeGroot Influence Problems using probabilistic model checking. Simul. Model. Pract. Theory 89, 144\u2013159 (2018)","journal-title":"Simul. Model. Pract. Theory"},{"issue":"5","key":"3018_CR39","doi-asserted-by":"crossref","first-page":"743","DOI":"10.3233\/JCS-140501","volume":"22","author":"M Arapinis","year":"2014","unstructured":"Arapinis, M., et al.: Statverif: verification of stateful processes. Journal of Computer Security 22(5), 743\u2013821 (2014)","journal-title":"Journal of Computer Security"},{"key":"3018_CR40","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"3018_CR41","first-page":"1","volume":"65","author":"MD Ryan","year":"2011","unstructured":"Ryan, M.D., Smyth, B.: Applied pi calculus. J ACM 65, 1 (2011)","journal-title":"J ACM"},{"issue":"4","key":"3018_CR42","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1109\/TSC.2015.2402679","volume":"9","author":"P Rodriguez-Mier","year":"2016","unstructured":"Rodriguez-Mier, P., et al.: An integrated semantic web service discovery and composition framework. IEEE Trans. Serv. Comput. 9(4), 537\u2013550 (2016)","journal-title":"IEEE Trans. Serv. Comput."},{"issue":"8","key":"3018_CR43","doi-asserted-by":"crossref","first-page":"3831","DOI":"10.1016\/j.eswa.2013.11.042","volume":"41","author":"A Souri","year":"2014","unstructured":"Souri, A., Jafari Navimipour, N.: Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Syst. Appl. 41(8), 3831\u20133849 (2014)","journal-title":"Expert Syst. Appl."},{"issue":"3","key":"3018_CR44","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1108\/K-02-2018-0092","volume":"48","author":"A Souri","year":"2019","unstructured":"Souri, A., et al.: A model checking approach for user relationship management in the social network. Kybernetes 48(3), 407\u2013423 (2019)","journal-title":"Kybernetes"},{"issue":"8","key":"3018_CR45","doi-asserted-by":"crossref","first-page":"2208","DOI":"10.1016\/j.asoc.2012.03.040","volume":"12","author":"X Zhao","year":"2012","unstructured":"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\u20132216 (2012)","journal-title":"Appl. Soft Comput."},{"issue":"7","key":"3018_CR46","doi-asserted-by":"crossref","first-page":"3409","DOI":"10.1016\/j.asoc.2012.12.033","volume":"13","author":"F Mardukhi","year":"2013","unstructured":"Mardukhi, F., et al.: QoS decomposition for service composition using genetic algorithm. Appl. Soft Comput. 13(7), 3409\u20133421 (2013)","journal-title":"Appl. Soft Comput."},{"key":"3018_CR47","unstructured":"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)"},{"key":"3018_CR48","doi-asserted-by":"crossref","first-page":"554","DOI":"10.1016\/j.procs.2015.04.083","volume":"50","author":"G Arunkumar","year":"2015","unstructured":"Arunkumar, G., Venkataraman, N.: A novel approach to address interoperability concern in cloud computing. Proc. Comput. Sci. 50, 554\u2013559 (2015)","journal-title":"Proc. Comput. Sci."},{"issue":"13","key":"3018_CR49","doi-asserted-by":"crossref","first-page":"5751","DOI":"10.1016\/j.eswa.2014.03.020","volume":"41","author":"R Rezaei","year":"2014","unstructured":"Rezaei, R., et al.: A semantic interoperability framework for software as a service systems in cloud computing environments. Expert Syst. Appl. 41(13), 5751\u20135770 (2014)","journal-title":"Expert Syst. Appl."},{"issue":"10","key":"3018_CR50","first-page":"e1947","volume":"30","author":"L Fatma","year":"2018","unstructured":"Fatma, L., Haithem, M.: Multicloud service composition: a survey of current approaches and issues. J. Softw. 30(10), e1947 (2018)","journal-title":"J. Softw."}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-019-03018-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10586-019-03018-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-019-03018-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,27]],"date-time":"2020-11-27T00:25:59Z","timestamp":1606436759000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10586-019-03018-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,28]]},"references-count":50,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["3018"],"URL":"https:\/\/doi.org\/10.1007\/s10586-019-03018-9","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"value":"1386-7857","type":"print"},{"value":"1573-7543","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,28]]},"assertion":[{"value":"9 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 July 2019","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 November 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 November 2019","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}