{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:43:09Z","timestamp":1740141789145,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2023,2]]},"DOI":"10.1007\/s10270-022-00990-6","type":"journal-article","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T08:07:07Z","timestamp":1648541227000},"page":"225-245","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal reconfiguration model for cloud resources"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4296-6893","authenticated-orcid":false,"given":"Aida","family":"Lahouij","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1920-1825","authenticated-orcid":false,"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0482-7254","authenticated-orcid":false,"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"990_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J., Mussat, L.: Introducing dynamic constraints in B. In: B\u201998: Recent Advances in the Development and Use of the B Method, Second International B Conference, Montpellier, France, 22\u201324 April 1998, Proceedings, pp. 83\u2013128 (1998)","DOI":"10.1007\/BFb0053357"},{"key":"990_CR2","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: The B Tool (Abstract), pp. 86\u201387. Springer, Berlin (1988). https:\/\/doi.org\/10.1007\/3-540-50214-9_8","DOI":"10.1007\/3-540-50214-9_8"},{"key":"990_CR3","volume-title":"The B-Book\u2014Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-Book\u2014Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"990_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"990_CR5","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"990_CR6","doi-asserted-by":"publisher","unstructured":"Al-Dhuraibi, Y., Paraiso, F., Djarallah, N., Merle, P.: Autonomic vertical elasticity of docker containers with elasticdocker. In: 2017 IEEE 10th International Conference on Cloud Computing (CLOUD), pp. 472\u2013479 (2017). https:\/\/doi.org\/10.1109\/CLOUD.2017.67","DOI":"10.1109\/CLOUD.2017.67"},{"key":"990_CR7","doi-asserted-by":"publisher","unstructured":"Al-Dhuraibi, Y., Zalila, F., Djarallah, N.B., Merle, P.: Coordinating vertical elasticity of both containers and virtual machines. In: CLOSER 2018\u20148th International Conference on Cloud Computing and Services Science. Funchal, Madeira, Portugal (2018).https:\/\/doi.org\/10.5220\/0006652403220329","DOI":"10.5220\/0006652403220329"},{"key":"990_CR8","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2017.2711009","author":"Y Al-Dhuraibi","year":"2017","unstructured":"Al-Dhuraibi, Y., Fawaz, P., Djarallah, N., Merle, P.: Elasticity in cloud computing: state of the art and research challenges. IEEE Trans. Serv. Comput. (2017). https:\/\/doi.org\/10.1109\/TSC.2017.2711009","journal-title":"IEEE Trans. Serv. Comput."},{"key":"990_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32885-5_15","volume-title":"Business Process Management","author":"M Amziani","year":"2012","unstructured":"Amziani, M., Melliti, T., Tata, S.: A generic framework for service-based business process elasticity in the cloud. In: Barros, A., Gal, A., Kindler, E. (eds.) Business Process Management. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-32885-5_15"},{"key":"990_CR10","doi-asserted-by":"publisher","unstructured":"Ashraf, A., Byholm, B., Porres, I.: Cramp: cost-efficient resource allocation for multiple web applications with proactive scaling. In: 4th IEEE International Conference on Cloud Computing Technology and Science Proceedings, pp. 581\u2013586 (2012). https:\/\/doi.org\/10.1109\/CloudCom.2012.6427605","DOI":"10.1109\/CloudCom.2012.6427605"},{"key":"990_CR11","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-74107-7_3","volume-title":"Logics of Specification Languages","author":"D Cansell","year":"2008","unstructured":"Cansell, D., M\u00e9ry, D.: The Event-B modelling method: concepts and case studies. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages, pp. 47\u2013152. Springer, Berlin (2008)"},{"key":"990_CR12","doi-asserted-by":"crossref","unstructured":"Chatziprimou, K., Lano, K., Zschaler, S.: Runtime infrastructure optimisation in cloud IaaS structures. In: 2013 IEEE 5th International Conference on Cloud Computing Technology and Science, vol.\u00a01, pp.\u00a0687\u2013692 (2013)","DOI":"10.1109\/CloudCom.2013.112"},{"key":"990_CR13","unstructured":"Chatziprimou, K., Lano, K., Zschaler, S.: Towards a meta-model of the cloud computing resource landscape. In: MODELSWARD (2013)"},{"key":"990_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/s12243-014-0450-7","author":"E Coutinho","year":"2014","unstructured":"Coutinho, E., Sousa, F., Rego, P., Gomes, D., Souza, J.: Elasticity in cloud computing: a survey. Ann. Telecommun. (2014). https:\/\/doi.org\/10.1007\/s12243-014-0450-7","journal-title":"Ann. Telecommun."},{"key":"990_CR15","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-642-22709-7_43","volume-title":"Advances in Computing and Communications","author":"W Dawoud","year":"2011","unstructured":"Dawoud, W., Takouna, I., Meinel, C.: Elastic VM for cloud resources provisioning optimization. In: Abraham, A., LloretMauri, J., Buford, J.F., Suzuki, J., Thampi, S.M. (eds.) Advances in Computing and Communications, pp. 431\u2013445. Springer, Berlin (2011)"},{"key":"990_CR16","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.future.2016.05.028","volume":"65","author":"S Farokhi","year":"2016","unstructured":"Farokhi, S., Jamshidi, P., Bayuh Lakew, E., Brandic, I., Elmroth, E.: A hybrid cloud controller for vertical memory elasticity: a control-theoretic approach. Future Gener. Comput. Syst. 65, 57\u201372 (2016). https:\/\/doi.org\/10.1016\/j.future.2016.05.028. (Special Issue on Big Data in the Cloud)","journal-title":"Future Gener. Comput. Syst."},{"key":"990_CR17","doi-asserted-by":"publisher","unstructured":"Fernandez, H., Pierre, G., Kielmann, T.: Autoscaling web applications in heterogeneous cloud infrastructures. In: 2014 IEEE International Conference on Cloud Engineering, pp. 195\u2013204 (2014). https:\/\/doi.org\/10.1109\/IC2E.2014.25","DOI":"10.1109\/IC2E.2014.25"},{"key":"990_CR18","doi-asserted-by":"publisher","unstructured":"Galante, G., de Bona, L.C.E.: A survey on cloud computing elasticity. In: 2012 IEEE Fifth International Conference on Utility and Cloud Computing, pp. 263\u2013270 (2012). https:\/\/doi.org\/10.1109\/UCC.2012.30","DOI":"10.1109\/UCC.2012.30"},{"issue":"6","key":"990_CR19","doi-asserted-by":"publisher","first-page":"987","DOI":"10.1007\/s00165-017-0425-3","volume":"29","author":"M Graiet","year":"2017","unstructured":"Graiet, M., Hamel, L., Mammar, A., Tata, S.: A verification and deployment approach for elastic component-based applications. Formal Asp. Comput. 29(6), 987\u20131011 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0425-3","journal-title":"Formal Asp. Comput."},{"key":"990_CR20","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.future.2013.12.037","volume":"35","author":"SM Gueye","year":"2014","unstructured":"Gueye, S.M., De Palma, N., Rutten, \u00c9., Tchana, A., Berthier, N.: Coordinating self-sizing and self-repair managers for multi-tier systems. Future Gener. Comput. Syst. 35, 14\u201326 (2014). https:\/\/doi.org\/10.1016\/j.future.2013.12.037. (Special Section: Integration of Cloud Computing and Body Sensor Networks; Guest Editors: Giancarlo Fortino and Mukaddim Pathan)","journal-title":"Future Gener. Comput. Syst."},{"key":"990_CR21","first-page":"211","volume-title":"An Introduction to the Event-B Modelling Method","author":"TS Hoang","year":"2013","unstructured":"Hoang, T.S.: An Introduction to the Event-B Modelling Method, pp. 211\u2013236. Springer, Berlin (2013)"},{"key":"990_CR22","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.jnca.2018.09.023","volume":"124","author":"W Iqbal","year":"2018","unstructured":"Iqbal, W., Erradi, A., Mahmood, A.: Dynamic workload patterns prediction for proactive auto-scaling of web applications. J. Netw. Comput. Appl. 124, 94\u2013107 (2018). https:\/\/doi.org\/10.1016\/j.jnca.2018.09.023","journal-title":"J. Netw. Comput. Appl."},{"key":"990_CR23","doi-asserted-by":"publisher","unstructured":"Kalyvianaki, E., Charalambous, T., Hand, S.: Self-adaptive and self-configured CPU resource provisioning for virtualized servers using Kalman filters. In: Proceedings of the 6th International Conference on Autonomic Computing, ICAC \u201909, pp. 117\u2013126. Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1555228.1555261","DOI":"10.1145\/1555228.1555261"},{"key":"990_CR24","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.ijar.2018.07.002","volume":"101","author":"S Kirthica","year":"2018","unstructured":"Kirthica, S., Sridhar, R.: A residue-based approach for resource provisioning by horizontal scaling across heterogeneous clouds. Int. J. Approx. Reason. 101, 88\u2013106 (2018). https:\/\/doi.org\/10.1016\/j.ijar.2018.07.002","journal-title":"Int. J. Approx. Reason."},{"key":"990_CR25","doi-asserted-by":"publisher","unstructured":"Lahouij, A., Hamel, L., Graiet, M., Malki, M.E.: A formal approach for cloud composite services verification. In: 11th IEEE Conference on Service-Oriented Computing and Applications, SOCA 2018, Paris, France, 20\u201322 Nov 2018, pp. 161\u2013168 (2018). https:\/\/doi.org\/10.1109\/SOCA.2018.00031","DOI":"10.1109\/SOCA.2018.00031"},{"key":"990_CR26","doi-asserted-by":"publisher","unstructured":"Lahouij, A., Hamel, L., Graiet, M.: Deadlock-freeness verification of cloud composite services using Event-B. In: On the Move to Meaningful Internet Systems. OTM 2018 Conferences\u2014Confederated International Conferences: CoopIS, C&TC, and ODBASE 2018, Valletta, Malta, 22\u201326 Oct 2018, Proceedings, Part I, pp. 604\u2013622 (2018). https:\/\/doi.org\/10.1007\/978-3-030-02610-3_34","DOI":"10.1007\/978-3-030-02610-3_34"},{"key":"990_CR27","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-64694-3_5","volume-title":"Reuse in Emerging Software Engineering Practices\u201419th International Conference on Software and Systems Reuse, ICSR 2020, Hammamet, Tunisia, 2\u20134 Dec 2020, Proceedings, Lecture Notes in Computer Science","author":"A Lahouij","year":"2020","unstructured":"Lahouij, A., Hamel, L., Graiet, M.: Dynamic reconfiguration of cloud composite services using Event-B. In: Sassi, S.B., Ducasse, S., Mili, H. (eds.) Reuse in Emerging Software Engineering Practices\u201419th International Conference on Software and Systems Reuse, ICSR 2020, Hammamet, Tunisia, 2\u20134 Dec 2020, Proceedings, Lecture Notes in Computer Science, vol. 12541, pp. 69\u201384. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-64694-3_5"},{"key":"990_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00517-0","author":"A Lahouij","year":"2020","unstructured":"Lahouij, A., Hamel, L., Graiet, M., Ayeb, B.E.: An Event-B based approach for cloud composite services verification. Formal Asp. Comput. (2020). https:\/\/doi.org\/10.1007\/s00165-020-00517-0","journal-title":"Formal Asp. Comput."},{"issue":"4","key":"990_CR29","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1016\/j.compind.2013.02.008","volume":"64","author":"Y Laili","year":"2013","unstructured":"Laili, Y., Tao, F., Zhang, L., Cheng, Y., Luo, Y., Sarker, B.R.: A ranking chaos algorithm for dual scheduling of cloud service and computing resource in private cloud. Comput. Ind. 64(4), 448\u2013463 (2013). https:\/\/doi.org\/10.1016\/j.compind.2013.02.008","journal-title":"Comput. Ind."},{"key":"990_CR30","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: Prob: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods, pp. 855\u2013874. Springer, Berlin (2003)"},{"key":"990_CR31","doi-asserted-by":"publisher","unstructured":"Marshall, P., Keahey, K., Freeman, T.: Elastic site: using clouds to elastically extend site resources. In: 2010 10th IEEE\/ACM International Conference on Cluster, Cloud and Grid Computing, pp. 43\u201352 (2010). https:\/\/doi.org\/10.1109\/CCGRID.2010.80","DOI":"10.1109\/CCGRID.2010.80"},{"key":"990_CR32","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.future.2014.10.017","volume":"50","author":"M Mohamed","year":"2014","unstructured":"Mohamed, M., Amziani, M., Bela\u00efd, D., Tata, S., Melliti, T.: An autonomic approach to manage elasticity of business processes in the cloud. Future Gener. Comput. Syst. 50, 49\u201361 (2014). https:\/\/doi.org\/10.1016\/j.future.2014.10.017","journal-title":"Future Gener. Comput. Syst."},{"key":"990_CR33","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-1-4471-6452-4_10","volume-title":"Survey of Elasticity Management Solutions in Cloud Computing","author":"A Najjar","year":"2014","unstructured":"Najjar, A., Serpaggi, X., Gravier, C., Boissier, O.: Survey of Elasticity Management Solutions in Cloud Computing, pp. 235\u2013263. Springer, London (2014). https:\/\/doi.org\/10.1007\/978-1-4471-6452-4_10"},{"key":"990_CR34","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-29919-8_12","volume-title":"Algorithmic Aspects of Cloud Computing","author":"A Naskos","year":"2016","unstructured":"Naskos, A., Gounaris, A., Sioutas, S.: Cloud elasticity: a survey. In: Karydis, I., Sioutas, S., Triantafillou, P., Tsoumakos, D. (eds.) Algorithmic Aspects of Cloud Computing, pp. 151\u2013167. Springer International Publishing, Cham (2016)"},{"key":"990_CR35","unstructured":"Padidar, S.: A study in the use of Event-B for system development from a software engineering viewpoint (2011) http:\/\/www.ai4fm.org\/papers\/MSc-Padidar.pdf"},{"issue":"5","key":"990_CR36","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/s00607-014-0421-x","volume":"98","author":"F Paraiso","year":"2016","unstructured":"Paraiso, F., Merle, P., Seinturier, L.: soCloud: a service-oriented component-based PaaS for managing portability, provisioning, elasticity, and high availability across multiple clouds. Computing 98(5), 539\u2013565 (2016). https:\/\/doi.org\/10.1007\/s00607-014-0421-x","journal-title":"Computing"},{"issue":"2","key":"990_CR37","doi-asserted-by":"publisher","first-page":"227","DOI":"10.2478\/amcs-2019-0017","volume":"29","author":"V Podolskiy","year":"2019","unstructured":"Podolskiy, V., Jindal, A., Gerndt, M.: Multilayered autoscaling performance evaluation: can virtual machines and containers co-scale? Int. J. Appl. Math. Comput. Sci. 29(2), 227\u2013244 (2019). https:\/\/doi.org\/10.2478\/amcs-2019-0017","journal-title":"Int. J. Appl. Math. Comput. Sci."},{"key":"990_CR38","doi-asserted-by":"publisher","unstructured":"Ramirez, Y.M., Podolskiy, V., Gerndt, M.: Capacity-driven scaling schedules derivation for coordinated elasticity of containers and virtual machines. In: 2019 IEEE International Conference on Autonomic Computing (ICAC), pp. 177\u2013186 (2019). https:\/\/doi.org\/10.1109\/ICAC.2019.00029","DOI":"10.1109\/ICAC.2019.00029"},{"key":"990_CR39","doi-asserted-by":"publisher","unstructured":"Shen, Z., Subbiah, S., Gu, X., Wilkes, J.: Cloudscale: elastic resource scaling for multi-tenant cloud systems. In: Proceedings of the 2nd ACM Symposium on Cloud Computing, SOCC \u201911. Association for Computing Machinery, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/2038916.2038921","DOI":"10.1145\/2038916.2038921"},{"key":"990_CR40","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/2150976.2151021","volume":"47","author":"N Vasi\u0107","year":"2012","unstructured":"Vasi\u0107, N., Novakovi\u0107, D., Miu\u010din, S., Kostic, D., Bianchini, R.: Dejavu: accelerating resource allocation in virtualized environments. ACM SIGPLAN Not. 47, 423\u2013436 (2012). https:\/\/doi.org\/10.1145\/2150976.2151021","journal-title":"ACM SIGPLAN Not."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-00990-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-00990-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-00990-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T06:39:29Z","timestamp":1677047969000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-00990-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,29]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["990"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-00990-6","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2022,3,29]]},"assertion":[{"value":"4 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 March 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}]}}