An Event-B based approach for cloud composite services verification
- PDF / 5,952,098 Bytes
- 33 Pages / 595.276 x 790.866 pts Page_size
- 36 Downloads / 261 Views
Formal Aspects of Computing
An Event-B based approach for cloud composite services verification Aida Lahouij1 , Lazhar Hamel2 , Mohamed Graiet3 and B´echir el Ayeb4 1 Universit´ e de Sousse, ISITCom, 4011 Hammam 2 ISIMM, Monastir University, Monastir, Tunisia 3 ENSAI RENNES, Bruz, France 4 FSM, Monastir University, Monastir, Tunisia
Sousse, Tunisia
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. Keywords: Formal verification, Cloud composite services, Semantic verification, Behavioral verification, Resource allocation, Event-B
1. Introduction In the last few years, there has been a growing interest in the verification of Cloud composite services especially with the emergence of the Cloud computing paradigm [FE10] and the additional challenges it brings. Service composition alone, without considering a Cloud environment, raises the need for designtime verification approaches to check the correctness of the interactions between the different components of a composite service. Indeed, the verification of the structural, semantic and behavioral matching of the component services involved in the composition is necessary in order to avoid the inconsistencies in the composite service and any possible deadlock situation that may occur during its execution. This task is not trivial especially with the deployment of the composite services in the Cloud, which adds the necessity to verify the Cloud resources allocated to the component services. Correspondence to: Aida Lahouij, e-mail: [email protected]
A. Lahouij et al.
In fact, the Cloud environment provides three types of resources: computing, networking, and storage. The resource’s elasticity and scalability are key features of the Cloud computing paradigm. A resource is elastic if it can change its capacity at runtime. Elasticity is the ability to dynamically increase or decre
Data Loading...
