{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:20:18Z","timestamp":1740122418973,"version":"3.37.3"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T00:00:00Z","timestamp":1622160000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T00:00:00Z","timestamp":1622160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s10586-021-03305-4","type":"journal-article","created":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T19:02:56Z","timestamp":1622228576000},"page":"2977-2994","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A model-based approach for formal verification and performance analysis of dynamic load-balancing protocols in cloud environment"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7941-158X","authenticated-orcid":false,"given":"Imene","family":"Ben Hafaiedh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roua","family":"Ben Hamouda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riadh","family":"Robbana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,28]]},"reference":[{"key":"3305_CR1","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.jnca.2017.04.007","volume":"88","author":"EJ Ghomi","year":"2017","unstructured":"Ghomi, E.J., Rahmani, A.M., Qader, N.N.: Load-balancing algorithms in cloud computing: a survey. J. Netw. Comput. Appl. 88, 50\u201371 (2017)","journal-title":"J. Netw. Comput. Appl."},{"key":"3305_CR2","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1016\/j.ijinfomgt.2018.07.009","volume":"43","author":"O Ali","year":"2018","unstructured":"Ali, O., et al.: Cloud computing-enabled healthcare opportunities, issues, and applications: a systematic review. Int. J. Inf. Manag. 43, 146\u2013158 (2018)","journal-title":"Int. J. Inf. Manag."},{"key":"3305_CR3","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1016\/j.ins.2017.09.033","volume":"422","author":"L Ferretti","year":"2018","unstructured":"Ferretti, L., et al.: A symmetric cryptographic scheme for data integrity verification in cloud databases. Inf. Sci. 422, 497\u2013515 (2018)","journal-title":"Inf. Sci."},{"key":"3305_CR4","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/j.future.2018.09.014","volume":"91","author":"AR Arunarani","year":"2019","unstructured":"Arunarani, A.R., Manjula, D., Vijayan, S.: Task scheduling techniques in cloud computing: a literature survey. Future Gener. Comput. Syst. 91, 407\u2013415 (2019)","journal-title":"Future Gener. Comput. Syst."},{"issue":"1","key":"3305_CR5","first-page":"1","volume":"38","author":"RK Jena","year":"2017","unstructured":"Jena, R.K.: Task scheduling in cloud environment: a multi-objective ABC framework. J. Inf. Optim. Sci. 38(1), 1\u201319 (2017)","journal-title":"J. Inf. Optim. Sci."},{"issue":"1","key":"3305_CR6","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10586-019-02928-y","volume":"23","author":"A Jyoti","year":"2020","unstructured":"Jyoti, A., Shrimali, M.: Dynamic provisioning of resources based on load balancing and service broker policy in cloud computing. Clust. Comput. 23(1), 377\u2013395 (2020)","journal-title":"Clust. Comput."},{"key":"3305_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.ins.2018.08.032","volume":"468","author":"W Lin","year":"2018","unstructured":"Lin, W., et al.: A cloud server energy consumption measurement system for heterogeneous cloud environments. Inf. Sci. 468, 47\u201362 (2018)","journal-title":"Inf. Sci."},{"doi-asserted-by":"crossref","unstructured":"Deepa, T., Cheelu, D.: A comparative study of static and dynamic load balancing algorithms in cloud computing. In: International Conference on Energy. Communication, Data Analytics and Soft Computing (ICECDS). IEEE (2017)","key":"3305_CR8","DOI":"10.1109\/ICECDS.2017.8390086"},{"unstructured":"Klaithem, N.A.: A survey of load balancing in cloud computing: Challenges and algorithms. In: Second Symposium on Network Cloud Computing and Applications, pp. 137\u2013142. IEEE (2012)","key":"3305_CR9"},{"key":"3305_CR10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.jnca.2017.08.020","volume":"98","author":"A Thakur","year":"2017","unstructured":"Thakur, A., Major, S.G.: A taxonomic survey on load balancing in cloud. J. Netw. Comput. Appl. 98, 43\u201357 (2017)","journal-title":"J. Netw. Comput. Appl."},{"issue":"3","key":"3305_CR11","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"doi-asserted-by":"crossref","unstructured":"Dellabani, M., Legay, A., Bensalem, S.: SBIP 2.0: statistical model checking stochastic real-time systems. Autom. Technol. Verif. Anal. 536\u2013542 (2018)","key":"3305_CR12","DOI":"10.1007\/978-3-030-01090-4_33"},{"issue":"2","key":"3305_CR13","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s10009-014-0313-6","volume":"17","author":"A Nouri","year":"2015","unstructured":"Nouri, A., et al.: Statistical model checking QoS properties of systems with SBIP. Int. J. Softw. Tools Technol. Transf. 17(2), 171\u2013185 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"unstructured":"Hafaiedh, I.B. et al.: Formal distributed model for the verification of job-scheduling in cloud environments. In: 2017 IEEE\/ACS 14th International Conference on Computer Systems and Applications (AICCSA). IEEE (2017)","key":"3305_CR14"},{"issue":"3","key":"3305_CR15","first-page":"321","volume":"16","author":"A Gawanmeh","year":"2015","unstructured":"Gawanmeh, A., Alomari, A.: Challenges in formal methods for testing and verification of cloud computing systems. Scalable Comput. 16(3), 321\u2013332 (2015)","journal-title":"Scalable Comput."},{"doi-asserted-by":"crossref","unstructured":"Bugingo, E. et al.: Towards decomposition based multi-objective workflow scheduling for big data processing in clouds. Clust. Comput. 1\u201325 (2020)","key":"3305_CR16","DOI":"10.1007\/s10586-020-03208-w"},{"key":"3305_CR17","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/TCC.2015.2474406","volume":"6","author":"L Wang","year":"2015","unstructured":"Wang, L., Gelenbe, E.: Adaptive dispatching of tasks in the cloud. IEEE Trans. Cloud Comput. 6, 33\u201345 (2015)","journal-title":"IEEE Trans. Cloud Comput."},{"key":"3305_CR18","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.simpat.2018.09.018","volume":"93","author":"E Barbierato","year":"2019","unstructured":"Barbierato, E., et al.: Exploiting CloudSim in a multiformalism modeling approach for cloud based systems. Simul. Model. Pract. Theory 93, 133\u2013147 (2019)","journal-title":"Simul. Model. Pract. Theory"},{"issue":"2","key":"3305_CR19","doi-asserted-by":"publisher","first-page":"2543","DOI":"10.1007\/s10586-017-1319-0","volume":"22","author":"H Cai","year":"2019","unstructured":"Cai, H., Hao, W.: An improved formalization analysis approach to determine schedulability of global multiprocessor scheduling based on symbolic safety analysis and statistical model checking in smartphone systems. Clust. Comput. 22(2), 2543\u20132554 (2019)","journal-title":"Clust. Comput."},{"doi-asserted-by":"crossref","unstructured":"Ishakian, V. et al.: Formal verification of SLA transformations. In: 2011 IEEE World Congress on Services. IEEE (2011)","key":"3305_CR20","DOI":"10.1109\/SERVICES.2011.16"},{"doi-asserted-by":"crossref","unstructured":"Blanchard, A. et al.: A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C. In: International Workshop on Formal Methods for Industrial Critical Systems. Springer (2015)","key":"3305_CR21","DOI":"10.1007\/978-3-319-19458-5_2"},{"doi-asserted-by":"crossref","unstructured":"Gao, J. et al.: SaaS performance and scalability evaluation in clouds. In: Proceedings of 2011 IEEE 6th International Symposium on Service Oriented System Engineering (SOSE), pp. 61\u201371. IEEE (2011)","key":"3305_CR22","DOI":"10.1109\/SOSE.2011.6139093"},{"issue":"4","key":"3305_CR23","doi-asserted-by":"publisher","first-page":"2453","DOI":"10.1007\/s10586-019-03018-9","volume":"23","author":"A Souri","year":"2020","unstructured":"Souri, A., et al.: A hybrid formal verification approach for QoS-aware multi-cloud service composition. Clust. Comput. 23(4), 2453\u20132470 (2020)","journal-title":"Clust. Comput."},{"key":"3305_CR24","volume-title":"International Conference on Formal Engineering Methods","author":"I Pereverzeva","year":"2013","unstructured":"Pereverzeva, I. et al.: Formal modelling of resilient data storage in cloud. In: International Conference on Formal Engineering Methods. Springer, Berlin (2013)"},{"doi-asserted-by":"crossref","unstructured":"Chen, J. et al.: A formal model for resource protections in web service applications. In: 2012 international conference on cloud and service computing. IEEE (2012)","key":"3305_CR25","DOI":"10.1109\/CSC.2012.24"},{"doi-asserted-by":"crossref","unstructured":"Hao, J., et al.: vTRUST: a formal modeling and verification framework for virtualization systems. In: International Conference on Formal Engineering Methods. Springer, Berlin (2013)","key":"3305_CR26","DOI":"10.1007\/978-3-642-41202-8_22"},{"doi-asserted-by":"crossref","unstructured":"Bleikertz, S., Thomas, G.: A virtualization assurance language for isolation and deployment. In: 2011 IEEE International Symposium on Policies for Distributed Systems and Networks. IEEE (2011)","key":"3305_CR27","DOI":"10.1109\/POLICY.2011.10"},{"doi-asserted-by":"crossref","unstructured":"Kikuchi, S., Yasuhide, M.: Performance modeling of concurrent live migration operations in cloud computing systems using Prism probabilistic model checker. In: 2011 IEEE 4th International Conference on Cloud Computing. IEEE (2011)","key":"3305_CR28","DOI":"10.1109\/CLOUD.2011.48"},{"issue":"4","key":"3305_CR29","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s11761-013-0148-0","volume":"8","author":"E Albert","year":"2014","unstructured":"Albert, E., et al.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Serv. Oriented Comput. Appl. 8(4), 323\u2013339 (2014)","journal-title":"Serv. Oriented Comput. Appl."},{"issue":"1","key":"3305_CR30","first-page":"23","volume":"41","author":"RN Calheiros","year":"2011","unstructured":"Calheiros, R.N., et al.: CloudSim: a Toolkit for modeling and simulation of cloud computing environments and evaluation of resource provisioning algorithms. Software 41(1), 23\u201350 (2011)","journal-title":"Software"},{"key":"3305_CR31","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1016\/j.ins.2017.02.054","volume":"397","author":"W Lin","year":"2017","unstructured":"Lin, W., et al.: Multi-resource scheduling and power simulation for cloud computing. Inf. Sci. 397, 168\u2013186 (2017)","journal-title":"Inf. Sci."},{"doi-asserted-by":"crossref","unstructured":"Neelima, P., Reddy, A.R.M.: An efficient load balancing system using adaptive dragonfly algorithm in cloud computing. Clust. Comput. 1\u20139 (2020)","key":"3305_CR32","DOI":"10.1007\/s10586-020-03054-w"},{"issue":"5","key":"3305_CR33","first-page":"595","volume":"43","author":"RN Calheiros","year":"2013","unstructured":"Calheiros, R.N., et al.: EMUSIM: an integrated emulation and simulation environment for modeling, evaluation, and validation of performance of cloud computing applications. Software 43(5), 595\u2013612 (2013)","journal-title":"Software"},{"doi-asserted-by":"crossref","unstructured":"Shetty, S.M., Shetty, S.: Analysis of load balancing in cloud data centers. J. Ambient Intell. Hum. Comput. 1\u20139 (2019)","key":"3305_CR34","DOI":"10.1007\/s12652-018-1106-7"},{"key":"3305_CR35","doi-asserted-by":"publisher","first-page":"1770","DOI":"10.1109\/TPDS.2016.2632713","volume":"28","author":"G Liu","year":"2017","unstructured":"Liu, G., Shen, H., Wang, H.: Towards long-view computing load balancing in cluster storage systems. IEEE Trans. Parallel Distrib. Syst. 28, 1770\u20131784 (2017)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"doi-asserted-by":"crossref","unstructured":"Jarraya, Y.: Cloud calculus: Security verification in elastic cloud computing platform. In: International Conference on Collaboration Technologies and Systems (CTS), pp. 447\u2013454. IEEE (2012)","key":"3305_CR36","DOI":"10.1109\/CTS.2012.6261089"},{"issue":"2","key":"3305_CR37","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1504\/IJCCBS.2018.096193","volume":"8","author":"IB Hafaiedh","year":"2018","unstructured":"Hafaiedh, I.B., Slimane, M.B., Robbana, R.: A formal model for the analysis and verification of a pre-emptive round-robin arbiter. Int. J. Crit. Comput.-Based Syst. 8(2), 169\u2013192 (2018)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"doi-asserted-by":"crossref","unstructured":"Falcone, Y. et al.: Runtime verification of component-based systems. In: International Conference on Software Engineering and Formal Methods. Springer, Berlin (2011)","key":"3305_CR38","DOI":"10.1007\/978-3-642-24690-6_15"},{"issue":"3\u20135","key":"3305_CR39","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.jlap.2010.10.001","volume":"80","author":"I Ben-Hafaiedh","year":"2011","unstructured":"Ben-Hafaiedh, I., Graf, S., Quinton, S.: Building distributed controllers for systems with priorities. J. Logic Algebraic Program. 80(3\u20135), 194\u2013218 (2011)","journal-title":"J. Logic Algebraic Program."},{"issue":"10","key":"3305_CR40","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors: Structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"3305_CR41","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/769782.769787","volume":"37","author":"K Yang","year":"2003","unstructured":"Yang, K., et al.: Towards efficient resource on-demand in grid computing. ACM SIGOPS Oper. Syst. Rev. 37(2), 37\u201343 (2003)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"doi-asserted-by":"crossref","unstructured":"Liu, L., Deyu, Q.: An independent task scheduling algorithm in heterogeneous multi-core processor environment. In: 2018 IEEE 3rd Advanced Information Technology, Electronic and Automation Control Conference (IAEAC). IEEE (2018)","key":"3305_CR42","DOI":"10.1109\/IAEAC.2018.8577208"},{"doi-asserted-by":"crossref","unstructured":"Choi, D., Chung, K.S., Shon, J.: An improvement on the weighted least-connection scheduling algorithm for load balancing in web cluster systems. In: Grid and Distributed Computing, Control and Automation, pp. 127\u2013134. Springer, Berlin (2010)","key":"3305_CR43","DOI":"10.1007\/978-3-642-17625-8_13"},{"doi-asserted-by":"crossref","unstructured":"Ren, X., Rongheng, L., Hua, Z.: A dynamic load balancing strategy for cloud computing platform based on exponential smoothing forecast. In: 2011 IEEE International Conference on Cloud Computing and Intelligence Systems (2011)","key":"3305_CR44","DOI":"10.1109\/CCIS.2011.6045063"},{"unstructured":"Lim, J.W., Hoong, P.K., Yeoh, E.T.: Heuristic neighbor selection algorithm for decentralized load balancing in clustered heterogeneous computational environment. In: 2012 14th International Conference on Advanced Communication Technology (ICACT), pp. 1215\u20131219. IEEE (2012)","key":"3305_CR45"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-021-03305-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10586-021-03305-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-021-03305-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T18:15:43Z","timestamp":1635617743000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10586-021-03305-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,28]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["3305"],"URL":"https:\/\/doi.org\/10.1007\/s10586-021-03305-4","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"type":"print","value":"1386-7857"},{"type":"electronic","value":"1573-7543"}],"subject":[],"published":{"date-parts":[[2021,5,28]]},"assertion":[{"value":"10 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 May 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}