research-article

Verification of a self-configuration protocol for distributed applications in the cloud

Authors:

Xavier Etchevers,

Fabienne Boyer,

Thierry CoupayeAuthors Info & Claims

SAC '12: Proceedings of the 27th Annual ACM Symposium on Applied Computing

Pages 1278 - 1283

https://doi.org/10.1145/2245276.2231979

Published: 26 March 2012 Publication History

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.

References

[1]

R. Allen, R. Douence, and D. Garlan. Specifying and Analyzing Dynamic Software Architectures. In Proc. of FASE'98, volume 1382 of LNCS, pages 21--37. Springer, 1998.

[2]

T. Barros, R. Ameur-Boulifa, A. Cansado, L. Henrio, and E. Madelaine. Behavioural Models for Distributed Fractal Components. Annales des Télécommunications, 64(1--2): 25--43, 2009.

[3]

L. Bellissard, N. D. Palma, A. Freyssinet, M. Herrmann, and S. Lacourte. An Agent Platform for Reliable Asynchronous Distributed Programming. In Proc. of SRDS'99, pages 294--295. IEEE Computer Society, 1999.

Digital Library

[4]

D. Bergamini, N. Descoubes, C. Joubert, and R. Mateescu. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. In Proc. of TACAS'05, volume 3440 of LNCS, pages 581--585. Springer, 2005.

Digital Library

[5]

M. Bozzano, A. Cimatti, J.-P. Katoen, V. Y. Nguyen, T. Noll, M. Roveri, and R. Wimmer. A Model Checker for AADL. In Proc. of CAV'10, volume 6174 of LNCS, pages 562--565. Springer, 2010.

Digital Library

[6]

D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, V. Powazny, F. Lang, W. Serwe, and G. Smeding. Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA/VASY, 2011.

[7]

C. Chapman, W. Emmerich, F. G. Márquez, S. Clayman, and A. Galis. Software Architecture Definition for On-demand Cloud Provisioning. In Proc. of HPDC'10, pages 61--72. ACM Press, 2010.

Digital Library

[8]

M. A. Cornejo, H. Garavel, R. Mateescu, and N. D. Palma. Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. In Proc. of DAIS'01, volume 198 of IFIP Conference Proceedings, pages 229--244. Kluwer, 2001.

Digital Library

[9]

H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In Proc. of TACAS'11, volume 6605 of LNCS, pages 372--387. Springer, 2011.

Digital Library

[10]

P. Goldsack, J. Guijarro, S. Loughran, A. Coles, A. Farrell, A. Lain, P. Murray, and P. Toft. The SmartFrog Configuration Management Framework. SIGOPS Oper. Syst. Rev., 43(1): 16--25, 2009.

Digital Library

[11]

J. Kramer and J. Magee. The Evolving Philosophers Problem: Dynamic Change Management. IEEE TSE, 16(11): 1293--1306, 1990.

Digital Library

[12]

J. Kramer and J. Magee. Analysing Dynamic Change in Distributed Software Architectures. IEE Proceedings - Software, 145(5): 146--154, 1998.

[13]

J. Magee, J. Kramer, and D. Giannakopoulou. Behaviour Analysis of Software Architectures. In Proc. of WICSA'99, volume 140 of IFIP Conference Proceedings, pages 35--50. Kluwer, 1999.

Digital Library

[14]

R. Mateescu and D. Thivolle. A Model Checking Language for Concurrent Value-Passing Systems. In Proc. of FM'08, volume 5014 of LNCS, pages 148--164. Springer, 2008.

Digital Library

[15]

J. Mirkovic, T. Faber, P. Hsieh, G. Malayandisamu, and R. Malavia. DADL: Distributed Application Description Language. USC/ISI Technical Report ISI-TR-664, 2010.

[16]

E. Vassev, M. Hinchey, and A. Quigley. Model Checking for Autonomic Systems Specified with ASSL. In Proc. of NFM'09, pages 16--25, 2009.

[17]

M. Wermelinger, A. Lopes, and J. L. Fiadeiro. A Graph Based Architectural (Re)configuration Language. In Proc. of ESEC/SIGSOFT FSE'01, pages 21--32. ACM Press, 2001.

Digital Library

Cited By

Etchevers XSalaün GBoyer FCoupaye TDeźPalma N(2019)Reliable self-deployment of distributed cloud applicationsSoftware—Practice & Experience10.1002/spe.240047:1(3-20)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1002/spe.2400
Salaün GBoyer FCoupaye TDe Palma NEtchevers XGruber O(2018)An experience report on the verification of autonomic protocols in the cloudInnovations in Systems and Software Engineering10.1007/s11334-013-0204-09:2(105-117)Online publication date: 15-Dec-2018
https://dl.acm.org/doi/10.1007/s11334-013-0204-0
Hafaiedh ISlimane MHaouala SRobbana R(2017)Formal Distributed Model for the Verification of Job-Scheduling in Cloud Environments2017 IEEE/ACS 14th International Conference on Computer Systems and Applications (AICCSA)10.1109/AICCSA.2017.144(660-667)Online publication date: Oct-2017
https://doi.org/10.1109/AICCSA.2017.144
Show More Cited By

Recommendations

Toward parameterized verification of synchronous distributed applications
SPIN 2014: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software

We present preliminary results on parameterized verification of distributed applications that assume a synchronous model of computation. Our theoretical results are negative -- the problem is undecidable even if each node has a single bit of non-...
The formal verification of a reintegration protocol
EMSOFT '05: Proceedings of the 5th ACM international conference on Embedded software

We report the first formal verification of a reintegration protocol for a safety-critical distributed embedded system. A reintegration protocol increases system survivability by allowing a transiently-faulty node to regain state. The protocol is ...
Hybrid Verification of Protocol Bridges

It is becoming increasingly more evident that simulation cannot provide full verification for today's complex designs. Formal verification is emerging as an alternative technique to simulation that promises to guarantee complete verification. However, ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '12: Proceedings of the 27th Annual ACM Symposium on Applied Computing

March 2012

2179 pages

ISBN:9781450308571

DOI:10.1145/2245276

Conference Chairs:
Sascha Ossowski
University Rey Juan Carlos, Spain
,
Paola Lecca
The Microsoft Research - University of Trento COSBI, Italy

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 March 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

SAC 2012

Sponsor:

SIGAPP

SAC 2012: ACM Symposium on Applied Computing

March 26 - 30, 2012

Trento, Italy

Acceptance Rates

SAC '12 Paper Acceptance Rate 270 of 1,056 submissions, 26%;

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
131
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Etchevers XSalaün GBoyer FCoupaye TDeźPalma N(2019)Reliable self-deployment of distributed cloud applicationsSoftware—Practice & Experience10.1002/spe.240047:1(3-20)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1002/spe.2400
Salaün GBoyer FCoupaye TDe Palma NEtchevers XGruber O(2018)An experience report on the verification of autonomic protocols in the cloudInnovations in Systems and Software Engineering10.1007/s11334-013-0204-09:2(105-117)Online publication date: 15-Dec-2018
https://dl.acm.org/doi/10.1007/s11334-013-0204-0
Hafaiedh ISlimane MHaouala SRobbana R(2017)Formal Distributed Model for the Verification of Job-Scheduling in Cloud Environments2017 IEEE/ACS 14th International Conference on Computer Systems and Applications (AICCSA)10.1109/AICCSA.2017.144(660-667)Online publication date: Oct-2017
https://doi.org/10.1109/AICCSA.2017.144
Salaün GYe L(2015)Debugging Process Algebra SpecificationsProceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 893110.1007/978-3-662-46081-8_14(245-262)Online publication date: 12-Jan-2015
https://dl.acm.org/doi/10.1007/978-3-662-46081-8_14
Durán FSalaün GSeinturier LAlmeida ECarlson J(2014)Robust reconfiguration of cloud applicationsProceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering10.1145/2602458.2602479(179-184)Online publication date: 27-Jun-2014
https://dl.acm.org/doi/10.1145/2602458.2602479
Etchevers XSalaün GBoyer FCoupaye TDe Palma NCho YShin SKim SHung CHong J(2014)Reliable self-deployment of cloud applicationsProceedings of the 29th Annual ACM Symposium on Applied Computing10.1145/2554850.2554951(1331-1338)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.1145/2554850.2554951
Garavel HLang FMateescu RSerwe W(2013)CADP 2011International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0244-z15:2(89-107)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1007/s10009-012-0244-z
Salaün GEtchevers XDe Palma NBoyer FCoupaye T(2013)Verification of a Self-configuration Protocol for Distributed Applications in the CloudAssurances for Self-Adaptive Systems10.1007/978-3-642-36249-1_3(60-79)Online publication date: 2013
https://doi.org/10.1007/978-3-642-36249-1_3
Abid RSalaün GBongiovanni FDe Palma N(2013)Verification of a Dynamic Management Protocol for Cloud ApplicationsAutomated Technology for Verification and Analysis10.1007/978-3-319-02444-8_14(178-192)Online publication date: 2013
https://doi.org/10.1007/978-3-319-02444-8_14

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents