{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T20:05:52Z","timestamp":1760299552441},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.<\/jats:p>","DOI":"10.1007\/s00165-017-0425-3","type":"journal-article","created":{"date-parts":[[2017,3,14]],"date-time":"2017-03-14T06:51:20Z","timestamp":1489474280000},"page":"987-1011","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["A verification and deployment approach for elastic component-based applications"],"prefix":"10.1145","volume":"29","author":[{"given":"Mohamed","family":"Graiet","sequence":"first","affiliation":[{"name":"High School of Computer Science and Mathematics, Monastir, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[{"name":"High School of Computer Science and Mathematics, Monastir, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amel","family":"Mammar","sequence":"additional","affiliation":[{"name":"SAMOVAR, T\u00e9l\u00e9com SudParis, CNRS, Universit\u00e9 Paris-Saclay, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Tata","sequence":"additional","affiliation":[{"name":"IBM Research - Almaden, 650 Harry Rd, 95120, San Jose, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11761-013-0148-0"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bersani M-M Bianculli D Dustdar S Gambi A Ghezzi C Krsti\u0107 S (2014) Towards the formalization of properties of cloud-based elastic systems. In: The 6th international workshop on principles of engineering service-oriented and cloud systems. ACM","DOI":"10.1145\/2593793.2593798"},{"key":"e_1_2_1_2_4_2","unstructured":"Booch G Rumbaugh J Jacobson I (2005) Unified modeling language user guide 2nd edn. Addison-Wesley Professional Reading"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chieu T-C Mohindra A Karve A-A Segal A (2009) Dynamic scaling of web applications in a virtualized cloud computing environment. In: The IEEE international conference on e-business engineering. IEEE Computer Society","DOI":"10.1109\/ICEBE.2009.45"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cok D-R (2011) JML for Java 7 by Extending OpenJDK. In: The 3rd international conference on NASA formal methods. Springer","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2011.07.005"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Dutta S Gera S Akshat V Viswanathan B (2012) SmartScale: automatic application scaling in enterprise clouds. In: The 5th international conference on cloud computing. IEEE Computer Society","DOI":"10.1109\/CLOUD.2012.12"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/MIC.2011.121"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2010.1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Galante G de Bona LCE (2012) A survey on cloud computing elasticity. In: The 5th international conference on utility and cloud computing. IEEE Computer Society","DOI":"10.1109\/UCC.2012.30"},{"key":"e_1_2_1_2_12_2","unstructured":"Geelan J Klems M Cohen R Kaplan J Gourlay D Gaw P Edwards D De Haaff B Kepes B Sheynkman K Sultan O Hartig K Pritzker J Doerksen T Von Eicken T Wallis P Sheehan M Dodge D Ricadela A Martin B Kepes B Berger I-W (2009) Twenty-one experts define cloud computing"},{"key":"e_1_2_1_2_13_2","unstructured":"Hamadi R Benatallah B (2003) A Petri net-based model for web service composition. In: The 14th Australasian database conference. Australian Computer Society"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"He S Guo L Guo Y Wu C Ghanem M Han R (2012) Elastic application container: a lightweight approach for cloud resource provisioning. In: AINA. IEEE Computer Society","DOI":"10.1109\/AINA.2012.74"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoenisch P Schulte S Dustdar S (2013) Workflow scheduling and resource allocation for cloud-based execution of elastic processes. In: The 6th international conference on service-oriented computing and applications. IEEE Computer Society","DOI":"10.1109\/SOCA.2013.44"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hoenisch P Schulte S Dustdar S Venugopal S (2013) Self-adaptive resource allocation for elastic process execution. In: The 6th international conference on cloud computing. IEEE","DOI":"10.1109\/CLOUD.2013.126"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Kranas P Anagnostopoulos V Menychtas A Varvarigou T-A (2012) ElaaS: an innovative elasticity as a service framework for dynamic management across the cloud stack layers. In: The 6th international conference on complex intelligent and software intensive systems. IEEE Computer Society","DOI":"10.1109\/CISIS.2012.117"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Klai K Tata S (2013) Formal modeling of elastic service-based business processes. In: International conference on services computing. IEEE Computer Society","DOI":"10.1109\/SCC.2013.75"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Butler M (2003) ProB: a model checker for B. Formal methods LNCS 2805","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Lahouij A Hamel L Graiet M (2013) Formal verification of SCA assembly model with Event-B. In: The 9th international conference on semantics knowledge and grids. IEEE Computer Society","DOI":"10.1109\/SKG.2013.31"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"L\u00ea L-S Linh Truong H Ghose A Dustdar S (2012) On elasticity and constrainedness of business services provisioning. In: The 9th international conference on services computing. IEEE Computer Society","DOI":"10.1109\/SCC.2012.34"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0323-x"},{"key":"e_1_2_1_2_23_2","unstructured":"Mammar A Graiet M Hamel L Tata S. http:\/\/www-public.tem-tsp.eu\/~mammar_a\/FACElasticity.html"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Mammar A Graiet M Hamel L Tata S (2016) A verification and deployment approach for elastic component-based applications. http:\/\/www-public.tem-tsp.eu\/~mammar_a\/FACElasticity.html","DOI":"10.1007\/s00165-017-0425-3"},{"key":"e_1_2_1_2_25_2","unstructured":"Marino J Rowley M (2009) Understanding SCA (Service Component Architecture). Addison-Wesley Professional Boston"},{"key":"e_1_2_1_2_26_2","unstructured":"OASIS (2011) OASIS. Architecture assembly model specification. Version 1.2. 19. http:\/\/docs.oasis-open.org\/opencsa\/sca-assembly\/sca-assembly-spec\/v1.2\/csd01\/sca-assembly-spec-v1.2-csd01.html"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3641"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Rivera V Cata\u00f1o N (2014) Translating Event-B to JML-specified java programs. In: The 29th annual ACM symposium on applied computing. ACM","DOI":"10.1145\/2554850.2554897"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Roy N Dubey A Gokhale A (2011) Efficient autoscaling in the cloud using predictive models for workload forecasting. In: The 4th international conference on cloud computing. IEEE Computer Society","DOI":"10.1109\/CLOUD.2011.42"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Sahli H Belala F Bouanaka C (2015) A BRS-based approach to model and verify cloud systems elasticity. In: 1st international conference on cloud forward: from distributed to complete computing","DOI":"10.1016\/j.procs.2015.09.221"},{"key":"e_1_2_1_2_31_2","unstructured":"Solanki M Cau A H Zedan H (2006) A wide spectrum language for designing web services. In: The 15th International World Wide Web Conference"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Schulte S Hoenisch P Venugopal S Dustdar S (2013) Introducing the Vienna platform for elastic processes. In: Workshops of international conference on service oriented computing. Springer","DOI":"10.1007\/978-3-642-37804-1_19"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Tsai W-T Sun X Shao Q Qi G (2010) Two-tier multi-tenancy scaling and load balancing. In: The 7th international conference on e-business engineering. IEEE Computer Society","DOI":"10.1109\/ICEBE.2010.103"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925861.1925869"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Yangui S Ben Nasrallah M Tata S (2013) PaaS-independent approach to provision appropriate cloud resources for SCA-based applications deployment. In: 9th international conference on semantics knowledge and grids","DOI":"10.1109\/SKG.2013.34"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s13174-010-0007-6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0425-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0425-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0425-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0425-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:14:06Z","timestamp":1641485646000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0425-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0425-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0425-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11]]}}}