{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:16Z","timestamp":1740109096753,"version":"3.37.3"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[2020,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The verification of the Cloud composite services\u2019 correctness is challenging. In fact, multiple component services, derived from different Cloud providers with different service description languages and communication protocols, are involved in the composition which may raise incompatibility issues that in turn lead to a non-consistent composition. In this work, we propose a formal approach to model and verify Cloud composite services. Four verification levels are considered in this article; the structural, semantic, behavioral, and resource allocation levels. Therefore, we opted for the Event-B formal method that enables complex problems decomposition thanks to its refinement capabilities. The proposed approach has proven its efficiency for the modelling and verification of Cloud composite services. The proposed model comprises four abstract levels with respect to the four verification axes. A proof-based approach is applied to the model\u2019s verification. We also succeeded in the validation of the model thanks to the model animation provided by the PROB tool. The use of formal methods provides a rigorous reasoning and mathematical proofs on the correction of the model which ensures the elaboration of correct-by-construction composite services.<\/jats:p>","DOI":"10.1007\/s00165-020-00517-0","type":"journal-article","created":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T04:07:50Z","timestamp":1600488470000},"page":"361-393","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An Event-B based approach for cloudcomposite services verification"],"prefix":"10.1145","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4296-6893","authenticated-orcid":false,"given":"Aida","family":"Lahouij","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Sousse, ISITCom, 4011, Hammam Sousse, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[{"name":"ISIMM, Monastir University, Monastir, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[{"name":"ENSAI RENNES, Bruz, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B\u00e9chir","family":"el Ayeb","sequence":"additional","affiliation":[{"name":"FSM, Monastir University, Monastir, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_2_2","first-page":"86","volume-title":"The B tool (Abstract)","author":"Abrial JR","year":"1988","unstructured":"AbrialJRThe B tool (Abstract)1988BerlinSpringer8687"},{"key":"e_1_2_1_2_3_2","volume-title":"The B-book\u2013assigning programs to meanings","author":"Abrial J-R","year":"2005","unstructured":"AbrialJ-RThe B-book\u2013assigning programs to meanings2005CambridgeCambridge University Press0915.68015"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abbassi I Graiet M Gaaloul W Hadj-Alouane NB (2015) Genetic-based approach for ATS and sla-aware web services composition. In: Web information systems engineering\u2014WISE 2015\u201416th international conference Miami FL USA November 1\u20133 2015 Proceedings Part I pp 369\u2013383","DOI":"10.1007\/978-3-319-26190-4_25"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Mussat L (1998) Introducing dynamic constraints in B. In: B'98: recent advances in the development and use of the B method second international B conference Montpellier France April 22\u201324 1998 Proceedings pp 83\u2013128","DOI":"10.1007\/BFb0053357"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.compeleceng.2016.08.006"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Abdelsadiq A Molina-Jimenez C Shrivastava S (2011) A high-level model-checking tool for verifying service agreements. In: Proceedings of 2011 IEEE 6th international symposium on service oriented system (SOSE) pp 297\u2013304","DOI":"10.1109\/SOSE.2011.6139120"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2011.05.001"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-319-69035-3_7","volume-title":"Service-oriented computing","author":"Boubaker S","year":"2017","unstructured":"BoubakerSKlaiKSchmitzKGraietMGaaloulWMaximilienMVallecilloAWangJOriolMDeadlock-freeness verification of business process configuration using SOGService-oriented computing2017ChamSpringer9611210.1007\/978-3-319-69035-3_7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2017.2667662"},{"issue":"65","key":"e_1_2_1_2_11_2","first-page":"01","article-title":"Scheduling strategies for business process applications in cloud environments","volume":"5","author":"Bessai K","year":"2014","unstructured":"BessaiKYoucefSOulamaraAGodartCNurcanSScheduling strategies for business process applications in cloud environmentsInt J Grid High Perform Comput2014565\u20137801","journal-title":"Int J Grid High Perform Comput"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chen J Huang L Huang H Yu C Li C (2012) A formal model for resource protections in web service applications. In: 2012 international conference on cloud and service computing pp 111\u2013118","DOI":"10.1109\/CSC.2012.24"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Cansell D M\u00e9ry D (2008) The event-b modelling method: concepts and case studies. pp 47\u2013152","DOI":"10.1007\/978-3-540-74107-7_3"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Cao Q Wei Z Gong W (2009) An optimized algorithm for task scheduling based on activity based costing in cloud computing. In: 2009 3rd international conference on bioinformatics and biomedical engineering pp 1\u20133","DOI":"10.1109\/ICBBE.2009.5162336"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n F Ouederni M Sala\u00fcn Gwen (July 2012) A generic framework for n-protocol compatibility checking. Sci Comput Program 77(7-8):870\u2013886","DOI":"10.1016\/j.scico.2011.03.009"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Elhag AAM Mohamad R Aziz MW Zeshan F (2015) A systematic composite service design modeling method using graph-based theory. PLoS One 10(4):1\u201326 04","DOI":"10.1371\/journal.pone.0123086"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-6524-0","volume-title":"Handbook of cloud computing","author":"Bo Furht","year":"2010","unstructured":"BoFurhtEscalanteAHandbook of cloud computing20101BerlinSpringer1214.68034","edition":"1"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Freitas L Watson P (2012) Formalising workflows partitioning over federated clouds: multi-level security and costs. In: 2012 IEEE eighth world congress on services pp 219\u2013226","DOI":"10.1109\/SERVICES.2012.75"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0425-3"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Graiet M Lahouij A Abbassi I Hamel L Kmimech M (2015) Formal behavioral modeling for verifying SCA composition with event-b. In: 2015 IEEE international conference on web services ICWS 2015 New York NY USA June 27\u2013July 2 2015 pp 17\u201324","DOI":"10.1109\/WETICE.2015.50"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2016.2594062"},{"key":"e_1_2_1_2_22_2","unstructured":"Hoang TS (2013) An introduction to the event-B modelling method pp 211\u2013236. 07"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_2_24_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: 2013 IEEE 6th international conference on service-oriented computing and applications pp 1\u20138","DOI":"10.1109\/SOCA.2013.44"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hoenisch P Schulte S Dustdar S Venugopal S (2013) Self-adaptive resource allocation for elastic process execution. In: 2013 IEEE sixth international conference on cloud computing pp 220\u2013227","DOI":"10.1109\/CLOUD.2013.126"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Jana B Chakraborty M Mandal T (2019) A task scheduling technique based on particle swarm optimization algorithm in cloud environment. In: Proceedings of SoCTA 2017 pp 525\u2013536. 01","DOI":"10.1007\/978-981-13-0589-4_49"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kallab L Mrissa M Chbeir R (2017) Bourreau Pierre Using colored petri nets for verifying restful service composition. In: Panetto H Debruyne C Gaaloul W Papazoglou M Paschke A Ardagna CA Meersman R (eds) On the move to meaningful internet systems. OTM 2017 conferences. Springer International Publishing Cham pp 505\u2013523","DOI":"10.1007\/978-3-319-69462-7_32"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Klai K Tata S Desel J (2009) Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl Eng 70(5):467\u2013482. In: Business Process Management 2011","DOI":"10.1016\/j.datak.2011.01.007"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: formal methods","author":"Leuschel M","year":"2003","unstructured":"LeuschelMButlerMArakiKGnesiSMandrioliDProb: a model checker for bFME 2003: formal methods2003BerlinSpringer85587410.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lahouij A Hamel L Graiet M (2015) Formal modeling for verifying SCA dynamic composition with event-b. In: 24th IEEE international conference on enabling technologies: infrastructure for collaborative enterprises WETICE 2015 Larnaca Cyprus June 15\u201317 2015 pp 29\u201334","DOI":"10.1109\/WETICE.2015.50"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Lahouij A Hamel L Graiet M Elkhalfa A Gaaloul W (2016) A global sla-aware approach for aggregating services in the cloud. In: On the move to meaningful internet systems: OTM 2016 conferences\u2014confederated international conferences: CoopIS C&TC and ODBASE 2016 Rhodes Greece October 24\u201328 2016 Proceedings pp 363\u2013380","DOI":"10.1007\/978-3-319-48472-3_21"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","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\u2014confederated international conferences: CoopIS C&TC and ODBASE 2018 Valletta Malta October 22-26 2018 Proceedings Part I pp 604\u2013622","DOI":"10.1007\/978-3-030-02610-3_34"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","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","DOI":"10.1109\/SOCA.2018.00031"},{"key":"e_1_2_1_2_34_2","unstructured":"Leesatapornwongsa T Hao M Joshi P Lukman JF Gunawi HS (2014) Samc: semantic-aware model checking for fast discovery of deep bugs in cloud systems. In: Proceedings of the 11th USENIX conference on operating systems design and implementation OSDI'14 pp 399\u2013414 Berkeley CA USA. USENIX Association"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.compind.2013.02.008"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Mastelic T Fdhila W Brandic I Rinderle-Ma S (2015) Predicting resource allocation and costs for business processes in the cloud. In: 2015 IEEE world congress on services pp 47\u201354","DOI":"10.1109\/SERVICES.2015.16"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCC.2013.3"},{"key":"e_1_2_1_2_38_2","unstructured":"Naskos A Stachtiari E Gounaris A Katsaros P Tsoumakos D Konstantinou I Sioutas S (2014) Cloud elasticity using probabilistic model checking. 05"},{"key":"e_1_2_1_2_39_2","unstructured":"Padidar S (2011) A study in the use of event-b for system development from a software engineering viewpoint"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Papapanagiotou P Fleuriot J (2011) Formal verification of web services composition using linear logic and the pi-calculus. In: 2011 IEEE ninth European conference on web services pp 31\u201338","DOI":"10.1109\/ECOWS.2011.18"},{"key":"e_1_2_1_2_41_2","first-page":"1","article-title":"Cloud service description model: an extension of usdl for cloud services","volume":"99","author":"Sun L","year":"2015","unstructured":"SunLMaJWangHZhangYCloud service description model: an extension of usdl for cloud servicesIEEE Trans Serv Comput20159911","journal-title":"IEEE Trans Serv Comput"},{"key":"e_1_2_1_2_42_2","unstructured":"W3C\u00a0Member Submission (2004) Owl-s: semantic markup for web services. https:\/\/www.w3.org\/Submission\/OWL-S\/"},{"key":"e_1_2_1_2_43_2","volume-title":"Using Z: specification, refinement, and proof","author":"Woodcock J","year":"1996","unstructured":"WoodcockJDaviesJUsing Z: specification, refinement, and proof1996Upper Saddle River, NJ, USAPrentice-Hall Inc0855.68060"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2015.2412943"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2013.2280559"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Zeng C Guo X Ou W Han D (2009) Cloud computing service composition and search based on semantic. In: Proceedings of the 1st international conference on cloud computing CloudCom '09 Springer Berlin pp 290\u2013300","DOI":"10.1007\/978-3-642-10665-1_26"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00517-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-020-00517-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00517-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00517-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,19]],"date-time":"2022-11-19T06:24:20Z","timestamp":1668839060000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00517-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":46,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["10.1007\/s00165-020-00517-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00517-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2020,11]]},"assertion":[{"value":"15 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 April 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 July 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 September 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}