Authors: Hamza Sahli; Faïza Belala; Chafia Bouanaka
Addresses: LIRE Laboratory, Constantine II University, Constantine, Algeria ' LIRE Laboratory, Constantine II University, Constantine, Algeria ' LIRE Laboratory, Constantine II University, Constantine, Algeria
Abstract: Cloud computing is a new delivery model based on a simple idea, which consists of providing a set of virtualised resources as on demand services that users can acquire according to their needs in an elastic way. In the context of preserving cloud systems elasticity and ensuring their reliability and consistency, formal methods can be very effective to model cloud systems and verify their inherent properties. Thus, we present in this paper a formal framework for specifying cloud systems and their elasticity methods. Furthermore, to show the usefulness of our BRS-based model, we propose two underlying formal approaches in order to verify the properties of elasticity and plasticity, while the first approach is based on the BigMC model-checker, the second one is based on judicious coupling between Maude language and BRS; in this case, the Maude LTL model-checker performs the verification.
Keywords: formal verification; model checking; cloud system elasticity; cloud computing; plasticity; bigraphical reactive systems; BRS; Maude.
International Journal of Critical Computer-Based Systems, 2016 Vol.6 No.4, pp.364 - 384
Published online: 26 Jan 2017 *Full-text access for editors Access for subscribers Purchase this article Comment on this article