An Event-B based approach for cloud composite services verification. (English) Zbl 1458.68014

Summary: The verification of the Cloud composite services’ 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’s 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.


68M11 Internet topics
68Q60 Specification and verification (program logics, model checking, etc.)


ProB; SPIN; Z; Rodin
Full Text: DOI


[1] Abrial, J-R; Butler, M.; Hallerstede, S.; Hoang, TS; Mehta, F.; Voisin, L., Rodin: an open toolset for modelling and reasoning in event-b, Int J Softw Tools Technol Transf, 12, 6, 447-466 (2010)
[2] Abrial, JR, The B tool (Abstract), 86-87 (1988), Berlin: Springer, Berlin
[3] Abrial, J-R, The B-book-assigning programs to meanings (2005), Cambridge: Cambridge University Press, Cambridge · Zbl 0915.68015
[4] 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—WISE 2015—16th international conference, Miami, FL, USA, November 1-3, 2015, Proceedings, Part I, pp 369-383
[5] 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-24, 1998, Proceedings, pp 83-128
[6] Amato, F.; Moscato, F., Pattern-based orchestration and automatic verification of composite cloud services, Comput & Electr Eng, 56, 842-853 (2016)
[7] 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-304
[8] Byun, E-K; Kee, Y-S; Kim, J-S; Maeng, S., Cost optimized provisioning of elastic resources for application workflows, Future Gener Comput Syst, 27, 8, 1011-1026 (2011)
[9] Boubaker, S.; Klai, K.; Schmitz, K.; Graiet, M.; Gaaloul, W.; Maximilien, M.; Vallecillo, A.; Wang, J.; Oriol, M., Deadlock-freeness verification of business process configuration using SOG, Service-oriented computing, 96-112 (2017), Cham: Springer, Cham
[10] Bourne, S.; Szabo, C.; Sheng, QZ, Transactional behavior verification in business process as a service configuration, IEEE Trans Serv Comput, 12, 2, 290-303 (2019)
[11] Bessai, K.; Youcef, S.; Oulamara, A.; Godart, C.; Nurcan, S., Scheduling strategies for business process applications in cloud environments, Int J Grid High Perform Comput, 5, 65-78, 01 (2014)
[12] 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-118
[13] Cansell D, Méry D (2008) The event-b modelling method: concepts and case studies. pp 47-152
[14] 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-3
[15] Durán F, Ouederni M, Salaün Gwen (July 2012) A generic framework for n-protocol compatibility checking. Sci Comput Program 77(7-8):870-886 · Zbl 1245.68028
[16] 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-26, 04
[17] Bo, Furht; Escalante, A., Handbook of cloud computing (2010), Berlin: Springer, Berlin · Zbl 1214.68034
[18] 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-226
[19] Graiet, M.; Hamel, L.; Mammar, A.; Tata, S., A verification and deployment approach for elastic component-based applications, Formal Asp Comput, 29, 6, 987-1011 (2017) · Zbl 1377.68039
[20] 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-July 2, 2015, pp 17-24
[21] Graiet, M.; Mammar, A.; Boubaker, S.; Gaaloul, W., Towards correct cloud resource allocation in business processes, IEEE Trans Serv Comput, 10, 1, 23-36 (2017)
[22] Hoang TS (2013) An introduction to the event-B modelling method, pp 211-236. 07
[23] Holzmann, GJ, The model checker spin, IEEE Trans Softw Eng, 23, 5, 279-295 (1997)
[24] 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-8
[25] 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-227
[26] 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-536. 01
[27] 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-523
[28] Klai K, Tata S, Desel J (2009) Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl Eng 70(5):467-482. In: Business Process Management, 2011
[29] Leuschel, M.; Butler, M.; Araki, K.; Gnesi, S.; Mandrioli, D., Prob: a model checker for b, FME 2003: formal methods, 855-874 (2003), Berlin: Springer, Berlin
[30] 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-17, 2015, pp 29-34
[31] 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—confederated international conferences: CoopIS, C&TC, and ODBASE 2016, Rhodes, Greece, October 24-28, 2016, Proceedings, pp 363-380
[32] 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-26, 2018, Proceedings, Part I, pp 604-622
[33] 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-22, 2018, pp 161-168
[34] 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-414, Berkeley, CA, USA. USENIX Association
[35] Laili, Y.; Tao, F.; Zhang, L.; Cheng, Y.; Luo, Y.; Sarker, BR, A ranking chaos algorithm for dual scheduling of cloud service and computing resource in private cloud, Comput Ind, 64, 4, 448-463 (2013)
[36] 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-54
[37] Malik, SUR; Khan, SU; Srinivasan, SK, Modeling and analysis of state-of-the-art vm-based cloud management platforms, IEEE Trans Cloud Comput, 1, 1, 1-1 (2013)
[38] Naskos A, Stachtiari E, Gounaris A, Katsaros P, Tsoumakos D, Konstantinou I, Sioutas S (2014) Cloud elasticity using probabilistic model checking. 05
[39] Padidar S (2011) A study in the use of event-b for system development from a software engineering viewpoint
[40] 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-38
[41] Sun, L.; Ma, J.; Wang, H.; Zhang, Y., Cloud service description model: an extension of usdl for cloud services, IEEE Trans Serv Comput, 99, 1-1 (2015)
[42] W3C Member Submission (2004) Owl-s: semantic markup for web services. https://www.w3.org/Submission/OWL-S/
[43] Woodcock, J.; Davies, J., Using Z: specification, refinement, and proof (1996), Upper Saddle River, NJ, USA: Prentice-Hall Inc, Upper Saddle River, NJ, USA · Zbl 0855.68060
[44] Wang, P.; Ding, Z.; Jiang, C.; Zhou, M.; Zheng, Y., Automatic web service composition based on uncertainty execution effects, IEEE Trans Serv Comput, 9, 4, 551-565 (2016)
[45] Wang, P.; Ding, Z.; Jiang, C.; Zhou, M., Constraint-aware approach to web service composition, IEEE Trans Syst Man Cybern Syst, 44, 6, 770-784 (2014)
[46] 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-300
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.