Abstract
One of the key characteristics of the Cloud environment is hight dynamicity; constantly new services are added and others are deleted due to unavailability, faulty behaviour or performance degradation. Cloud services can be packaged together and offered as a composite service to overcome the atomic service’s shortage or respond to specific user demand. In this context, a faulty component service must be dynamically replaced in order to preserve the functional and non-functional correctness of the composite service. This work presents a formal approach to verify the dynamic behaviour of the Cloud composite service. We mainly focus on the correctional dynamic such as the substitution of faulty or unavailable services and resources. The proposed Event-B approach ensures the preservation of the composite service consistency, reliability and efficiency after the substitution of faulty or unavailable components.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
For more details on proof obligations rules please refer to the B-Book [3] on page 190.
References
Abid, R., Salaün, G., De Palma, N.: Formal design of dynamic reconfiguration protocol for cloud applications. Sci. Comput. Program. 117, 1–16 (2016). https://doi.org/10.1016/j.scico.2015.12.001. http://www.sciencedirect.com/science/article/pii/S0167642315004128
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_8
Abrial, J.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
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_32
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/BFb0053357
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. MTCSAES, pp. 47–152. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74107-7_3
Furht, B., Escalante, A.: Handbook of Cloud Computing, 1st edn. Springer, Heidelberg (2010). https://doi.org/10.1007/978-1-4419-6524-0
Gao, H., Duan, Y., Miao, H., Yin, Y.: An approach to data consistency checking for the dynamic replacement of service process. IEEE Access 5, 11700–11711 (2017)
Gao, H., Huang, W., Yang, X., Duan, Y., Yin, Y.: Toward service selection for workflow reconfiguration: an interface-based computing solution. Future Gener. Comput. Syst. 87, 298–311 (2018). https://doi.org/10.1016/j.future.2018.04.064. http://www.sciencedirect.com/science/article/pii/S0167739X17320575
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, June 27–July 2, 2015, pp. 17–24 (2015)
Lahouij, A., Hamel, L., Graiet, M.: Formal modeling for verifying SCA dynamic composition with Event-B. In: 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, pp. 29–34 (2015)
Lahouij, A., Hamel, L., Graiet, M.: 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 (2018). https://doi.org/10.1007/978-3-030-02610-3_34
Lahouij, A., Hamel, L., Graiet, M., el Ayeb, B.: An Event-B based approach for cloud composite services verification. Form. Asp. Comput. 1–33 (2020). https://doi.org/10.1007/s00165-020-00517-0
Lahouij, A., Hamel, L., Graiet, M., Malki, M.E.: 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 (2018). https://doi.org/10.1109/SOCA.2018.00031
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). https://doi.org/10.1016/j.compind.2013.02.008. http://www.sciencedirect.com/science/article/pii/S0166361513000365
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Meng, S., Fu, G.: A formal design model for cloud services, pp. 173–178 (July 2017). https://doi.org/10.18293/SEKE2017-055
Padidar, S.: A study in the use of Event-B for system development from a software engineering viewpoint (2011). http://www.ai4fm.org/papers/MSc-Padidar.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Lahouij, A., Hamel, L., Graiet, M. (2020). Dynamic Reconfiguration of Cloud Composite Services Using Event-B. In: Ben Sassi, S., Ducasse, S., Mili, H. (eds) Reuse in Emerging Software Engineering Practices. ICSR 2020. Lecture Notes in Computer Science(), vol 12541. Springer, Cham. https://doi.org/10.1007/978-3-030-64694-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-64694-3_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-64693-6
Online ISBN: 978-3-030-64694-3
eBook Packages: Computer ScienceComputer Science (R0)