Top

Published in:

2018 | OriginalPaper | Chapter

Deadlock-Freeness Verification of Cloud Composite Services Using Event-B

Authors : Aida Lahouij, Lazhar Hamel, Mohamed Graiet

Published in: On the Move to Meaningful Internet Systems. OTM 2018 Conferences

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

With the emergence of the Cloud computing paradigm, interests were focused on representing and verifying the Cloud architecture in a formal way in order to prevent eventual failures and deadlocks. Service composition promotes reuse, interoperability, and loosely coupled interaction. However, verifying the correctness of a composite service remains a tedious task. To ensure the correctness of a composition, critical properties such as deadlock freeness must be verified. In this paper, we propose a novel formal approach to verify Cloud composite services correctness based on the Event-B method. We consider that both behavioral incompatibilities and conflicted resource may lead the composite service execution to failure. Event-B provides rigorous mathematical reasoning that helps building trust on developed software. A verification and validation approach combining both model proofs and model checking is finally performed to check the soundness of the proposed model.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Context-Aware Predictive Process Monitoring: The Impact of News Sentiment

next chapter A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics

Event-B and the Rodin platform. http://www.event-b.org/

Abdelsadiq, A., Molina-Jimenez, C., Shrivastava, S.: 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, December 2011

Abrial, J.R.: The B tool (abstract). In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds.) VDM 1988. LNCS, vol. 328, pp. 86–87. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-50214-9_8CrossRef

Abrial, J.R.: Faultless systems: yes we can! Computer 42(9), 30–36 (2009)CrossRef

Abrial, J.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)MATH

Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_32CrossRef

Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053357CrossRef

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.) ICSOC 2017. LNCS, vol. 10601, pp. 96–112. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-69035-3_7CrossRef

Cansell, D., Méry, D.: The Event-B modelling method: concepts and case studies. In: BjØrner, D., Henson, M.C. (eds.) Logics of Specification Languages. EATCS, pp. 47–152. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74107-7_3CrossRefMATH

10.

Chen, J., Huang, L., Huang, H., Yu, C., Li, C.: A formal model for resource protections in web service applications. In: 2012 International Conference on Cloud and Service Computing, pp. 111–118, November 2012

11.

Durán, F., Ouederni, M., Salaün, G.: A generic framework for n-protocol compatibility checking. Sci. Comput. Program. 77(7–8), 870–886 (2012)CrossRef

12.

Freitas, L., Watson, P.: Formalising workflows partitioning over federated clouds: multi-level security and costs. In: 2012 IEEE Eighth World Congress on Services, pp. 219–226, June 2012

13.

Furht, B., Escalante, A.: Handbook of Cloud Computing, 1st edn. Springer, Boston (2010). https://doi.org/10.1007/978-1-4419-6524-0CrossRefMATH

14.

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)CrossRef

15.

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)MathSciNetCrossRef

16.

Graiet, M., Lahouij, A., Abbassi, I., Hamel, L., Kmimech, M.: Formal behavioral modeling for verifying SCA composition with Event-B. In: 2015 IEEE International Conference on Web Services, ICWS 2015, New York, NY, USA, 27 June–2 July 2015, pp. 17–24 (2015)

17.

Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef

18.

Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl. Eng. 70(5), 467–482 (2011). Business Process Management 2009CrossRef

19.

Lahouij, A., Hamel, L., Graiet, M.: 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, 15–17 June 2015, pp. 29–34 (2015)

20.

Lahouij, A., Hamel, L., Graiet, M., Elkhalfa, A., Gaaloul, W.: A global SLA-aware approach for aggregating services in the cloud. In: Debruyne, C. (ed.) OTM 2016. LNCS, vol. 10033, pp. 363–380. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48472-3_21CrossRef

21.

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)CrossRef

22.

Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J.F., Gunawi, H.S.: 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 2014, pp. 399–414. USENIX Association, Berkeley (2014)

23.

Lemos, A.L., Daniel, F., Benatallah, B.: Web service composition: a survey of techniques and tools. ACM Comput. Surv. 48(3), 33:1–33:41 (2015)CrossRef

24.

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 (2013)CrossRef

25.

Naskos, A., et al.: Cloud elasticity using probabilistic model checking, May 2014

26.

Padidar, S.: A study in the use of Event-B for system development from a software engineering viewpoint. http://www.ai4fm.org/papers/MSc-Padidar.pdf

27.

Papapanagiotou, P., Fleuriot, J.: 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, September 2011

28.

Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall Inc., Upper Saddle River (1996)MATH

29.

Yang, Y., Tan, Q., Xiao, Y.: Verifying web services composition based on hierarchical colored petri nets. In: Proceedings of the First International Workshop on Interoperability of Heterogeneous Information Systems, IHIS 2005, pp. 47–54. ACM, New York (2005)

Title: Deadlock-Freeness Verification of Cloud Composite Services Using Event-B
Authors: Aida Lahouij
Lazhar Hamel
Mohamed Graiet
Publisher: Springer International Publishing
Book: On the Move to Meaningful Internet Systems. OTM 2018 Conferences
Print ISBN: 978-3-030-02609-7

Electronic ISBN: 978-3-030-02610-3

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-02610-3_34

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner