A formal approach for the correct deployment of cloud applications

The 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 reusing and reducing 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 EVENT-B-based approach for the modeling 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 through 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.

Automated summary

This paper introduces a formal EVENT-B-based approach for modeling and verifying the deployment of component-based applications. By gradually refining an abstract model, a precise specification is built, and mathematical reasoning is used to prove its correctness. The presented approach validates the deployment in a cloud environment using PROB and ensures the construction of a correct system that meets the constraints.