A formal approach for correct elastic package-based free and open source software composition in cloud

Abstract

Cloud environments have been increasingly used to deploy and run software while providing a high level performance with a low operating cost. Most of the existing software applications are nowadays distributed as Package-based Free and Open Source (PFOS) applications. Different requirements must be considered while configuring PFOS software. These requirements can be classified into two classes: dependency and capacity requirements. In this paper, we proposed a novel approach to ensure the correctness of elastic composite PFOS applications. Our approach is based on Event-B and combines proof-based models with model checking to provide a more complete verification. It starts by abstractly specifying the main concepts of PFOS software, and then refining them through multiple steps to model the elastic composite PFOS software and its correctness requirements. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we used the ProB model-checker to trace possible design errors.