An Event-B based approach for cloudcomposite services verification

• Published in: Formal aspects of computing 2020-11, Vol.32 (4-6), p.361-393
• Main Authors: Lahouij, Aida, Hamel, Lazhar, Graiet, Mohamed, el Ayeb, Béchir
• Format: Article
• Language: English
• ISSN: 0934-5043; 1433-299X
• DOI: 10.1007/s00165-020-00517-0

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.