Formal verification of cloud systems elasticity
by Hamza Sahli; Faïza Belala; Chafia Bouanaka
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 6, No. 4, 2016

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.

Online publication date: Thu, 26-Jan-2017

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com