{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:47:43Z","timestamp":1740142063575,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"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":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,3]]},"DOI":"10.1007\/s11334-021-00419-1","type":"journal-article","created":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T21:02:35Z","timestamp":1637787755000},"page":"85-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Event-B model for dynamically managing cloud resources"],"prefix":"10.1007","volume":"18","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":[[2021,11,24]]},"reference":[{"key":"419_CR1","volume-title":"The B-book: assigning programs to meanings","author":"J Abrial","year":"2005","unstructured":"Abrial J (2005) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge"},{"key":"419_CR2","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 (2010) Modeling in event-B: system and software engineering, cambridge. Cambridge University Press, Cambridge","edition":"cambridge"},{"key":"419_CR3","doi-asserted-by":"publisher","unstructured":"Al\u00a0dhuraibi Y, Fawaz P, Djarallah N, Merle P (06 2017) Elasticity in cloud computing: state of the art and research challenges. IEEE Trans Serv Comput PP, 1. https:\/\/doi.org\/10.1109\/TSC.2017.2711009","DOI":"10.1109\/TSC.2017.2711009"},{"key":"419_CR4","doi-asserted-by":"publisher","unstructured":"Al-Dhuraibi Y, Paraiso F, Djarallah N, Merle P (2017) Autonomic vertical elasticity of docker containers with elasticdocker. In: 2017 IEEE 10th international conference on cloud computing (CLOUD). pp 472\u2013479. https:\/\/doi.org\/10.1109\/CLOUD.2017.67","DOI":"10.1109\/CLOUD.2017.67"},{"key":"419_CR5","doi-asserted-by":"crossref","unstructured":"Al-Dhuraibi Y, Zalila F, Djarallah NB, Merle P (2018) Coordinating vertical elasticity of both containers and virtual machines. In: CLOSER 2018\u20148th international conference on cloud computing and services science. Funchal, Madeira, Portugal, https:\/\/hal.archives-ouvertes.fr\/hal-01683041","DOI":"10.5220\/0006652403220329"},{"key":"419_CR6","doi-asserted-by":"publisher","unstructured":"Ashraf A, Byholm B, Porres I (2012) 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. https:\/\/doi.org\/10.1109\/CloudCom.2012.6427605","DOI":"10.1109\/CloudCom.2012.6427605"},{"key":"419_CR7","doi-asserted-by":"crossref","unstructured":"Dawoud W, Takouna I, Meinel C (2011) Elastic vm for cloud resources provisioning optimization. In: Abraham A, Lloret Mauri J, Buford JF, Suzuki J, Thampi SM (eds) Advances in computing and communications. Springer, Berlin, pp 431\u2013445","DOI":"10.1007\/978-3-642-22709-7_43"},{"key":"419_CR8","unstructured":"Event-B and the rodin platform. http:\/\/www.event-b.org\/. Accessed 31 Aug 2021"},{"key":"419_CR9","doi-asserted-by":"publisher","unstructured":"Farokhi S, Jamshidi P, Bayuh Lakew E, Brandic I, Elmroth E (2016) A hybrid cloud controller for vertical memory elasticity: a control-theoretic approach. Future Gener Comput Syst 65:57\u201372. https:\/\/doi.org\/10.1016\/j.future.2016.05.028","DOI":"10.1016\/j.future.2016.05.028"},{"key":"419_CR10","doi-asserted-by":"publisher","unstructured":"Fernandez H, Pierre G, Kielmann T (2014) Autoscaling web applications in heterogeneous cloud infrastructures. In: 2014 IEEE international conference on cloud engineering. pp 195\u2013204. https:\/\/doi.org\/10.1109\/IC2E.2014.25","DOI":"10.1109\/IC2E.2014.25"},{"issue":"1","key":"419_CR11","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/TSC.2010.1","volume":"3","author":"W Gaaloul","year":"2010","unstructured":"Gaaloul W, Bhiri S, Rouached M (2010) Event-based design and runtime verification of composite service transactional behavior. IEEE Trans Serv Comput 3(1):32\u201345","journal-title":"IEEE Trans Serv Comput"},{"issue":"6","key":"419_CR12","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 (2017) A verification and deployment approach for elastic component-based applications. Formal Aspects Comput 29(6):987\u20131011. https:\/\/doi.org\/10.1007\/s00165-017-0425-3","journal-title":"Formal Aspects Comput"},{"key":"419_CR13","unstructured":"Hamadi R, Benatallah B (2003) A petri net-based model for web service composition. In: Schewe KD, Zhou X (eds) ADC\u20192003. CRPIT, vol.\u00a017, pp 191\u2013200. Australian Computer Society"},{"key":"419_CR14","unstructured":"Hoang TS (07 2013) an introduction to the event-B modelling method, pp 211\u2013236"},{"key":"419_CR15","doi-asserted-by":"publisher","unstructured":"Iqbal W, Erradi A, Mahmood A (2018) Dynamic workload patterns prediction for proactive auto-scaling of web applications. J Netw Comput Appl 124:94\u2013107. https:\/\/doi.org\/10.1016\/j.jnca.2018.09.023","DOI":"10.1016\/j.jnca.2018.09.023"},{"key":"419_CR16","doi-asserted-by":"publisher","unstructured":"Kirthica S, Sridhar R (2018) A residue-based approach for resource provisioning by horizontal scaling across heterogeneous clouds. Int J Approx Reason 101:88\u2013106. https:\/\/doi.org\/10.1016\/j.ijar.2018.07.002","DOI":"10.1016\/j.ijar.2018.07.002"},{"key":"419_CR17","doi-asserted-by":"publisher","unstructured":"Lahouij A, Hamel L, Graiet M (2018) Deadlock-freeness verification of cloud composite services using event-b. In: On the move to meaningful internet systems. OTM 2018 Conferences - confederated international conferences: CoopIS, C&TC, and ODBASE 2018, Valletta, Malta, October 22\u201326, 2018, Proceedings, Part I. pp 604\u2013622. https:\/\/doi.org\/10.1007\/978-3-030-02610-3_34","DOI":"10.1007\/978-3-030-02610-3_34"},{"key":"419_CR18","doi-asserted-by":"publisher","unstructured":"Lahouij A, Hamel L, Graiet M (2020) Dynamic reconfiguration of cloud composite services using event-b. In: Sassi SB, Ducasse S, Mili H (eds) Reuse in emerging software engineering practices - 19th international conference on software and systems reuse, ICSR 2020, Hammamet, Tunisia, December 2\u20134, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12541, pp 69\u201384. Springer. https:\/\/doi.org\/10.1007\/978-3-030-64694-3_5","DOI":"10.1007\/978-3-030-64694-3_5"},{"key":"419_CR19","doi-asserted-by":"publisher","unstructured":"Lahouij A, Hamel L, Graiet M, Ayeb BE (2020) An event-b based approach for cloud composite services verification. Formal Aspects of Computing. https:\/\/doi.org\/10.1007\/s00165-020-00517-0","DOI":"10.1007\/s00165-020-00517-0"},{"key":"419_CR20","doi-asserted-by":"publisher","unstructured":"Lahouij A, Hamel L, Graiet M, Malki ME (2018) A formal approach for cloud composite services verification. In: 11th IEEE conference on service-oriented computing and applications, SOCA 2018, Paris, France, November 20\u201322, 2018. pp 161\u2013168. https:\/\/doi.org\/10.1109\/SOCA.2018.00031","DOI":"10.1109\/SOCA.2018.00031"},{"key":"419_CR21","doi-asserted-by":"publisher","unstructured":"Laili Y, Tao F, Zhang L, Cheng Y, Luo Y, Sarker BR (2013) A ranking chaos algorithm for dual scheduling of cloud service and computing resource in private cloud. Comput Ind 64(4):448\u2013463. https:\/\/doi.org\/10.1016\/j.compind.2013.02.008","DOI":"10.1016\/j.compind.2013.02.008"},{"key":"419_CR22","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) Prob: a model checker for b. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods. Springer, Berlin, pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"issue":"3","key":"419_CR23","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s10270-008-0098-8","volume":"8","author":"A Mammar","year":"2009","unstructured":"Mammar A (2009) A systematic approach to generate B preconditions: application to the database domain. Softw Syst Model 8(3):385\u2013401","journal-title":"Softw Syst Model"},{"key":"419_CR24","doi-asserted-by":"publisher","unstructured":"Mohamed M, Amziani M, Bela\u00efd D, Tata S, Melliti T (2015) An autonomic approach to manage elasticity of business processes in the cloud. Future Gener Comput Syst 50, 49\u201361. https:\/\/doi.org\/10.1016\/j.future.2014.10.017","DOI":"10.1016\/j.future.2014.10.017"},{"key":"419_CR25","unstructured":"Padidar S (2011) A study in the use of event-b for system development from a software engineering viewpoint, http:\/\/www.ai4fm.org\/papers\/MSc-Padidar.pdf"},{"key":"419_CR26","doi-asserted-by":"publisher","unstructured":"Podolskiy V, Jindal A, Gerndt M (2019) Multilayered autoscaling performance evaluation: can virtual machines and containers co-scale? Int J Appl Math Comput Sci 29(2): 227 \u2013 244. https:\/\/doi.org\/10.2478\/amcs-2019-0017","DOI":"10.2478\/amcs-2019-0017"},{"key":"419_CR27","doi-asserted-by":"publisher","unstructured":"Ramirez YM, Podolskiy V, Gerndt M (2019) 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. https:\/\/doi.org\/10.1109\/ICAC.2019.00029","DOI":"10.1109\/ICAC.2019.00029"},{"key":"419_CR28","doi-asserted-by":"publisher","unstructured":"Sahli H, Bouanaka C, Dib ATE (2014) Towards a formal model for cloud computing elasticity. In: 2014 IEEE 23rd international WETICE conference, pp 359\u2013364. https:\/\/doi.org\/10.1109\/WETICE.2014.18","DOI":"10.1109\/WETICE.2014.18"},{"key":"419_CR29","doi-asserted-by":"publisher","unstructured":"Shahidinejad A, Ghobaei-Arani M, Esmaeili L (2020) An elastic controller using colored petri nets in cloud computing environment. Clust Comput 23. https:\/\/doi.org\/10.1007\/s10586-019-02972-8","DOI":"10.1007\/s10586-019-02972-8"},{"key":"419_CR30","doi-asserted-by":"crossref","unstructured":"Solanki M, Cau A, Zedan H (2006) ASDL: a wide spectrum language for designing web services. In: Carr L, Roure DD, Iyengar A, Goble CA, Dahlin M (eds) WWW\u20192006. pp 687\u2013696. ACM","DOI":"10.1145\/1135777.1135878"},{"key":"419_CR31","doi-asserted-by":"publisher","unstructured":"Vasi\u0107 N, Novakovi\u0107 D, Miu\u010din S, Kostic D, Bianchini R (04 2012) Dejavu: accelerating resource allocation in virtualized environments. ACM SIGPLAN Notices 47. https:\/\/doi.org\/10.1145\/2150976.2151021","DOI":"10.1145\/2150976.2151021"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00419-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-021-00419-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00419-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,22]],"date-time":"2022-05-22T08:05:17Z","timestamp":1653206717000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-021-00419-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,24]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,3]]}},"alternative-id":["419"],"URL":"https:\/\/doi.org\/10.1007\/s11334-021-00419-1","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2021,11,24]]},"assertion":[{"value":"20 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}