Title: Formal verification of cloud systems elasticity

 

Author: 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

 

Journal: Int. J. of Critical Computer-Based Systems, 2016 Vol.6, No.4, pp.364 - 384

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2016.081809

 

Available online 25 Jan 2017

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article