Verification of a Self-configuration Protocol for Distributed Applications in the Cloud

Gwen Salaün; Xavier Etchevers; Noël De Palma; Fabienne Boyer; Thierry Coupaye

hal-00685394, version 1

Verification of a Self-configuration Protocol for Distributed Applications in the Cloud

Gwen Salaün ¹, Xavier Etchevers ², Noël De Palma ^3, 4, Fabienne Boyer ^3, 4, Thierry Coupaye ⁵

27th Symposium On Applied Computing (SAC 2012) (2012) 1278-1283

Abstract: Distributed applications in the cloud are composed of a set of virtual machines running a set of interconnected software components. In this context, the task of automatically configuring distributed applications is a very difficult issue. In this paper, we focus on such a self-configuration protocol, which is able to configure a whole distributed application without requiring any centralized server. The high degree of parallelism involved in this protocol makes its design complicated and error-prone. In order to check that this protocol works as expected, we specify it in LOTOS NT and verify it using the CADP toolbox. The use of these formal techniques and tools helped to detect a bug in the protocol, and served as a workbench to experiment with several possible communication models.

1: CONVECS (INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble)
INRIA – Université Joseph Fourier - Grenoble I – CNRS : UMR5217 – Institut polytechnique de Grenoble (Grenoble INP) – Laboratoire d'Informatique de Grenoble : LIG
2: Orange Labs [Grenoble]
France Telecom RD
3: Université Joseph Fourier (Grenoble 1 UJF)
Université Joseph Fourier - Grenoble I
4: Laboratoire d'Informatique de Grenoble (LIG)
Université Joseph Fourier - Grenoble I – Institut Polytechnique de Grenoble - Grenoble Institute of Technology – Université Pierre-Mendès-France - Grenoble II – CNRS : UMR5217
5: France Télécom Recherche & Développement (FT R&D)
France Télécom

hal-00685394, version 1
http://hal.archives-ouvertes.fr/hal-00685394
oai:hal.archives-ouvertes.fr:hal-00685394
From: Gwen Salaün <>
Submitted on: Thursday, 5 April 2012 08:43:38
Updated on: Thursday, 5 April 2012 14:43:04

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00685394"><analytic>
<author><persName><forename>Gwen</forename><surname>Salaün</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">CONVECS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Laboratoire d'Informatique de Grenoble : LIG</orgName>
</affiliation>
</author>
<author><persName><forename>Xavier</forename><surname>Etchevers</surname></persName>
<affiliation>
<orgName type="team">Orange Labs [Grenoble]</orgName>
<country>FR</country>
<orgName type="institution">France Telecom RD</orgName>
</affiliation>
</author>
<author><persName><forename>Noël</forename><surname>De Palma</surname></persName>
<affiliation>
<orgName type="laboratory">Grenoble 1 UJF</orgName>
<orgName type="team">Université Joseph Fourier</orgName>
<country>FR</country>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LIG</orgName>
<orgName type="team">Laboratoire d'Informatique de Grenoble</orgName>
<country>FR</country>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Institut Polytechnique de Grenoble - Grenoble Institute of Technology</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Fabienne</forename><surname>Boyer</surname></persName>
<affiliation>
<orgName type="laboratory">Grenoble 1 UJF</orgName>
<orgName type="team">Université Joseph Fourier</orgName>
<country>FR</country>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LIG</orgName>
<orgName type="team">Laboratoire d'Informatique de Grenoble</orgName>
<country>FR</country>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Institut Polytechnique de Grenoble - Grenoble Institute of Technology</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Thierry</forename><surname>Coupaye</surname></persName>
<affiliation>
<orgName type="laboratory">FT R&D</orgName>
<orgName type="team">France Télécom Recherche & Développement</orgName>
<country>FR</country>
<orgName type="institution">France Télécom</orgName>
</affiliation>
</author>
<title type="main" level="a">Verification of a Self-configuration Protocol for Distributed Applications in the Cloud</title></analytic><monogr><title level="m" type="main">Proceedings of SAC 2012</title><meeting>27th Symposium On Applied Computing (SAC 2012)</meeting><imprint><pubPlace><country>Italy</country></pubPlace><biblScope type="publicationDate">2012-03-26</biblScope><biblScope type="pp">1278-1283</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00685394</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00685394/PDF/SEBCP-SAC12.pdf</idno></biblStruct>
</listBibl>
</listBibl>