Grenoble INP (FRANCE)
University Joseph Fourier, Grenoble (FRANCE)
Inria Grenoble - Rhône-Alpes / CONVECS project-team (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
2200 lines of LNT
600 reconfiguration scenarios
35 temporal logic properties
Cloud computing is a new programming paradigm that emerged a few years
ago, which aims at delivering resources and software applications over
a network (such as the Internet). Cloud computing leverages hosting
platforms based on virtualization and promotes a new software licensing
and billing model based on the pay-per-use concept. Cloud
applications are inherently distributed and run on different virtual
machines (VMs). Therefore, to deploy their applications, cloud users
need first to instantiate several virtual machines. Moreover, during
the application life time, various management operations may be
required, such as instantiating new VMs, replicating some of them for
load balancing purposes, destroying or replacing VMs, etc.
We propose a novel protocol for (re)configuring distributed applications in cloud environments. These applications consist of interconnected software components hosted on several VMs. A deployment manager guides the reconfiguration tasks by instantiating new VMs or destroying existing ones. After instantiation, each VM tries to satisfy its required services (ports) by binding its components to other components providing these services. When a VM receives a destruction request from the deployment manager, that VM unbinds and stops its components. In order to (un)bind/start/stop components, VMs communicate together through a publish/subscribe communication media.
Designing such protocols is a complicated task because they involve a high degree of parallelism, making it very difficult to anticipate all execution scenarios. Therefore, we followed a rigorous design process, based on formal methods and verification, to ensure that the protocol satisfies certain key properties. We specified the protocol in LNT, as well as over 600 hand-crafted examples (application model and reconfiguration scenario). We also identified 35 temporal properties that the protocol must respect during its execution, and specified them in MCL. For each example, we generated the Labelled Transition System (LTS) model from the LNT specification and verified all the MCL properties on it using the EVALUATOR model checker of the CADP toolbox.
The use of verification techniques helped us to improve the protocol.
For instance, in an initial version of the protocol, the component
start-up/shutdown was guided by a centralised deployment manager.
We observed an explosion in terms of states/transitions in the
corresponding LTSs, even for simple examples involving few VMs.
This was due to an overhead of messages transmitted to and from the
deployment manager, which was supposed to keep track of all
modifications in each VM to possibly start/stop components.
To avoid this problem, we proposed a decentralised version of the protocol, where each VM is in charge of starting and stopping its own components. We also detected a major bug in the VM destruction process. Originally, when it was required to stop a component, it was stopped before the components bound to it. This typically violates some architectural invariants (e.g., a started component cannot be connected to a stopped component) and impedes the robustness level expected from the protocol. We corrected this issue by stopping properly components, which required a deep revision of the protocol. Thus, in the current version of the protocol, when a component must be stopped, it requests to all the components connected to it to unbind and once it is done, it can finally stop.
R. Abid, G. Salaün, F. Bongiovanni, and N. De Palma.
Verification of a Dynamic Management Protocol for Cloud Applications.
Proceedings of the 11th International Symposium on Automated Technology
for Verification and Analysis ATVA'2013 (Hanoi, Vietnam), October 2013.
Available on-line at: http://hal.inria.fr/hal-00863262/en
or from our FTP site in PDF and PostScript
[Abid-Salaun-dePalma-15] R. Abid, G. Salaün, and N. de Palma. "Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications". Science of Computer Programming, 117:1-16, 2016.
Available on-line at: http://hal.inria.fr/hal-01246152/en
or from our FTP site in PDF and PostScript
Inria and LIG - CONVECS project-team
655, av. de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 54 28
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case-study, amongst others, is described on the CADP Web Page site: http://cadp.inria.fr/case-studies|