naa a22 4500 510791271 CHVBK 20180411083320.0 cr unu---uuuuu 180411e20130601xx s 000 0 eng 10.1007/s11334-013-0204-0 doi (NATIONALLICENCE)springer-10.1007/s11334-013-0204-0 An experience report on the verification of autonomic protocols in the cloud [Elektronische Daten] [Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noel De Palma, Xavier Etchevers, Olivier Gruber] 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 3years. Springer-Verlag London, 2013 Salaün Gwen Grenoble INP, Inria, France aut Boyer Fabienne UJF, Grenoble, France aut Coupaye Thierry Orange Labs, Issy-les-Moulineaux, France aut De Palma Noel UJF, Grenoble, France aut Etchevers Xavier Orange Labs, Issy-les-Moulineaux, France aut Gruber Olivier UJF, Grenoble, France aut Innovations in Systems and Software Engineering Springer-Verlag 9/2(2013-06-01), 105-117 1614-5046 9:2<105 2013 9 11334 https://doi.org/10.1007/s11334-013-0204-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s11334-013-0204-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Salaün Gwen Grenoble INP, Inria, France aut NATIONALLICENCE 700 1- Boyer Fabienne UJF, Grenoble, France aut NATIONALLICENCE 700 1- Coupaye Thierry Orange Labs, Issy-les-Moulineaux, France aut NATIONALLICENCE 700 1- De Palma Noel UJF, Grenoble, France aut NATIONALLICENCE 700 1- Etchevers Xavier Orange Labs, Issy-les-Moulineaux, France aut NATIONALLICENCE 700 1- Gruber Olivier UJF, Grenoble, France aut NATIONALLICENCE 773 0- Innovations in Systems and Software Engineering Springer-Verlag 9/2(2013-06-01), 105-117 1614-5046 9:2<105 2013 9 11334 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer