Self-configuration Protocol for the Cloud

Organisation:	INRIA Rhône-Alpes, Grenoble University Joseph Fourier, Grenoble Grenoble INP Orange Labs, Grenoble (FRANCE)
Method:	LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Cloud Computing.
Period:	2011
Size:	n/a.
Description:	Cloud computing emerged a few years ago as a major topic in modern programming. It leverages hosting platforms based on virtualization, and promises to deliver resources and applications that are faster and cheaper with a new software licensing and billing model based on the pay-per-use concept. Distributed applications in the cloud are made up of several virtual machines (VMs) that execute interconnected software elements. From a user perspective, deploying such applications goes through several steps: instantiation of images, selected in the IaaS repository, as VMs in the cloud; post-configuration of the booted VMs to set up the dynamic part of the application configuration; activation of the application, which generally requires to start the VMs in a given order so that the applicative components embedded in the VMs are activated at the right time. These configuration and activation tasks are a real burden as the VMs often include many software configuration parameters. Some of them refer to local configuration aspects (e.g., pool size, authentication data) whereas others participate in the definition of the interconnections between the remote elements (e.g., IP address and port to access a server). Therefore, once it has been instantiated, each virtual machine has to apply a set of dynamic settings in order to properly configure the distributed application. On the whole, existing deployment solutions hardly take into account these different configuration parameters, which are mostly managed thanks to dedicated (i.e., application specific) and not completely automated scripts (i.e., human intervention is needed). Moreover, such solutions enforce many requirements that delineate the spectrum of distributed applications they can deploy. This case-study deals with an innovative self-configuration protocol that automates the deployment of distributed applications in the cloud. The protocol, which is designed to be generic, decentralized, and loosely-coupled, is supported by a platform named VAMP (Virtual Applications Management Platform). The high degree of parallelism involved in this protocol makes its design complicated and error-prone, requiring the usage of formal methods and verification. After specifying the self-configuration protocol in LNT, this specification was applied to a set of distributed applications to be configured. From the specification and the target application, the CADP tools generate an LTS describing all possible executions of the protocol. The first verification consists in checking that each input application respects certain structural properties (e.g., there is no cycle in the application through mandatory client interfaces, all mandatory client interfaces are connected, etc.). This is checked at the beginning of the protocol using functions which extract the relevant information from the application model and display it as parameters to specific actions. Then, the absence of actions carrying wrong parameters is checked using a safety property. In a second step, 14 correctness properties of the protocol are expressed in MCL and verified using the EVALUATOR 4.0 model checker of CADP. Finally, it is checked that the behaviour of each VM isolated from the whole LTS respects the correct ordering of actions, by means of the BISIMULATOR equivalence checker of CADP.
Conclusions:	The formal modeling in LNT and verification using CADP helped to detect a major bug in the self-configuration protocol, which was corrected in the reference implementation in JAVA. The LNT specification also served as a workbench to experiment with several possible communication models, and these experiments were helpful in avoiding an erroneous design.
Publications:	[Etchevers-Coupaye-Boyer-et-al-11] Xavier Etchevers, Thierry Coupaye, Fabienne Boyer, Noël de Palma, and Gwen Salaün. "Automated Configuration of Legacy Applications in the Cloud". Proceedings of the 4th IEEE/ACM International Conference on Utility and Cloud Computing UCC'2012 (Melbourne, Australia), December 2011. Available on-line from http://cadp.inria.fr/publications/Etchevers-Coupaye-Boyer-et-al-11.html and from the CADP Web site in PDF or PostScript [Salaun-Etchevers-dePalma-et-al-12] Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, and Thierry Coupaye. "Verification of a Self-configuration Protocol for Distributed Applications in the Cloud". Proceedings of the 27th Symposium on Applied Computing SAC'2012 (Riva del Garda, Italy), ACM Press, March 2012. Available on-line from the CADP Web site in PDF or PostScript [Salaun-Etchevers-dePalma-et-al-13] Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, and Thierry Coupaye. "Verification of a Self-configuration Protocol for Distributed Applications in the Cloud". In Assurances for Self-Adaptive Systems, Springer Verlag, January 2013. Available on-line from http://hal.inria.fr/hal-00806914 and from the CADP Web site in PDF or PostScript [Salaun-Boyer-Coupaye-et-al-13] Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma, Xavier Etchevers, and Olivier Gruber. "An Experience Report on the Verification of Autonomic Protocols in the Cloud". In Innovations in Systems and Software Engineering, April 2013. Available on-line from http://hal.inria.fr/hal-00808565 and from the CADP Web site in PDF or PostScript [Etchevers-Salaun-Boyer-Coupaye-dePalma-14] Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, and Noël de Palma. "Reliable Self-Deployment of Cloud Applications". Proceedings of the 29th ACM Symposium on Applied Computing SAC'2014 (Gyeongju, Korea), March 2014. Available on-line from https://hal.inria.fr/hal-00934042 and from the CADP Web site in PDF or PostScript [Etchevers-Salaun-Boyer-Coupaye-dePalma-17] Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, and Noël de Palma. "Reliable Self-Deployment of Distributed Cloud Applications". In Software Practice and Experience 47(1):3-20, 2017. Available on-line from https://hal.inria.fr/hal-01290465 and from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün INRIA Rhône-Alpes / VASY 655, avenue de l'Europe F-38330 Montbonnot Saint Martin France Tel: +33 (0)4 76 61 54 28 Fax: +33 (0)4 76 61 52 52 Email: Gwen.Salaun@inria.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page