Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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 Transf 12(6), 447–466 (2010)
Abrial, J.R.: The B tool (Abstract), pp. 86–87. Springer, Berlin (1988)
Abrial, J.-R.: The B-book–assigning programs to meanings. Cambridge University Press, Cambridge (2005)
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
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
Amato, F., Moscato, F.: Pattern-based orchestration and automatic verification of composite cloud services. Comput & Electr Eng 56, 842–853 (2016)
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
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)
Boubaker, S., Klai, K., Schmitz, K., Graiet, M., Gaaloul, W.: Deadlock-freeness verification of business process configuration using SOG. In: Maximilien, M., Vallecillo, A., Wang, J., Oriol, M. (eds.) Service-oriented computing, pp. 96–112. Springer, Cham (2017)
Bourne, S., Szabo, C., Sheng, Q.Z.: Transactional behavior verification in business process as a service configuration. IEEE Trans Serv Comput 12(2), 290–303 (2019)
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)
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
Cansell D, Méry D (2008) The event-b modelling method: concepts and case studies. pp 47–152
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
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
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
Bo, Furht, Escalante, A.: Handbook of cloud computing, 1st edn. Springer, Berlin (2010)
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
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)
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
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)
Hoang TS (2013) An introduction to the event-B modelling method, pp 211–236. 07
Holzmann, G.J.: The model checker spin. IEEE Trans Softw Eng 23(5), 279–295 (1997)
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
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
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
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
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
Leuschel, M., Butler, M.: Prob: a model checker for b. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: formal methods, pp. 855–874. Springer, Berlin (2003)
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
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
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
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
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
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–463 (2013)
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
Malik, S.U.R., Khan, S.U., Srinivasan, S.K.: Modeling and analysis of state-of-the-art vm-based cloud management platforms. IEEE Trans Cloud Comput 1(1), 1–1 (2013)
Naskos A, Stachtiari E, Gounaris A, Katsaros P, Tsoumakos D, Konstantinou I, Sioutas S (2014) Cloud elasticity using probabilistic model checking. 05
Padidar S (2011) A study in the use of event-b for system development from a software engineering viewpoint
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
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)
W3C Member Submission (2004) Owl-s: semantic markup for web services. https://www.w3.org/Submission/OWL-S/
Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall Inc, Upper Saddle River, NJ, USA (1996)
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)
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)
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
Author information
Authors and Affiliations
Corresponding author
Additional information
Michael Butler
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Lahouij, A., Hamel, L., Graiet, M. et al. An Event-B based approach for cloud composite services verification. Form Asp Comp 32, 361–393 (2020). https://doi.org/10.1007/s00165-020-00517-0
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-020-00517-0