A Formal approach for the correct deployment of cloud applications

Overview & Synopsis

Deployment of cloud applications is a complex task. It refers to the enablement of SaaS, PaaS or IaaS solutions that may be accessed on demand by end users. It encompasses all the activities from installation to uninstallation, including reconfiguration, etc. To facilitate the deployment of cloud applications, it is essential to design them as component-based applications in order to favor the design by reuse and reduce the development cost. However, assembling components can be a tedious and error-prone task if sufficient precautions are not taken regarding different constraints, dependencies, and conflicts between components. In this paper, we introduce a formal \eventB-based approach for the modelling and the verification of component-based applications deployment. Our goal is to build correct by-construction systems that fulfill the different constraints regarding the components, the cloud infrastructure, and the deployment process. Basically, our approach starts with an abstract model describing the main concepts of the system. Then different details are gradually introduced by refinement. For each refinement step, proof obligations are produced to ensure the model's correctness. The obtained formal model consists of a precise specification on which mathematical reasoning can be carried out to prove the correctness of our component-based application model and validate its deployment in a cloud environment by using \ProB. The presented approach is illustrated through a case study.