An Experience Report on the Verification of Autonomic Protocols in the Cloud

Gwen Salaün (1) , Fabienne Boyer (2, 3) , Thierry Coupaye (4) , Noël de Palma (2, 3) , Xavier Etchevers (5) , Olivier Gruber (3)

1 CONVECS - Construction of verified concurrent systems
2 UJF - Université Joseph Fourier - Grenoble 1
3 LIG - Laboratoire d'Informatique de Grenoble
4 FT R&D - France Télécom Recherche & Développement
5 Orange Labs [Meylan]

Cloud applications are often complex distributed applications composed of multiple software components running on separate virtual machines. Setting up, (re)configuring, and monitoring these applications are complicated tasks because a software application may depend on several remote software and virtual machine configurations. These management tasks involve many complex protocols, which fully automate these tasks while preserving application consistency as well as some key properties. In this article, we present two experiences we had in formally specifying and verifying such protocols. The first one aims at designing a reconfiguration protocol of a component-based platform, intended as the foundation for building robust dynamic systems. The second aims at automating the configuration task of a set of virtual machines running a set of interconnected software components. Both applications are specified using the LNT process algebra and verified using the CADP verification toolbox. The use of formal specification languages and tools was a success. We conclude with a number of lessons we have learned while working on this topic in the last three years.

Domaines: Génie logiciel [cs.SE]

Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma, Xavier Etchevers, et al.. An Experience Report on the Verification of Autonomic Protocols in the Cloud. Innovations in Systems and Software Engineering, 2013, ⟨10.1007/s11334-013-0204-0⟩. ⟨hal-00808565⟩