[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

An experience report on the verification of autonomic protocols in the cloud

  • SI: SAC-SVT’12
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

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 3 years.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. This work results from a collaboration between experts in autonomic protocols and cloud computing on the one hand, and an expert in formal techniques and tools on the other. More precisely, the repartition of the work was as follows: The reconfiguration protocol (Sect. 2.1) was designed by F. Boyer and O. Gruber; The self-configuration protocol (Sect. 2.2) was designed by X. Etchevers, N. De Palma, F. Boyer, and T. Coupaye; Specification and verification tasks (Sect. 3) were carried out by G. Salaün.

  2. OpenCloudware is a French project that started in 2012, involving many companies and research centers in France, see http://opencloudware.org for more details.

  3. This work started in September 2009 and the first version of this article was submitted in July 2012.

  4. Since the number of VMs depends on the application, this LNT process is generated automatically for each new application by a Python program we wrote.

  5. This syntax has been defined by the model-driven architecture (MDA) initiative of the Object Management Group (OMG).

References

  1. Allen R, Douence R, Garlan D (1998) Specifying and analyzing dynamic software architectures. In: Proceedings of FASE’98, volume 1382 of LNCS. Springer, Berlin, pp 21–37

  2. Andova S, Groenewegen L, Stafleu J, de Vink EP (2009) Formalizing adaptation on-the-fly. Electron Notes Theor Comp Sci 255: 23–44

    Google Scholar 

  3. Arbab F (2004) Reo: a channel-based coordination model for component composition. Math Struct Comp Sci 14(3):329–366

    Article  MathSciNet  MATH  Google Scholar 

  4. Barros T, Ameur-Boulifa R, Cansado A, Henrio L, Madelaine E (2009) Behavioural models for distributed fractal components. Ann des Télécommun 64(1–2):25–43

    Article  Google Scholar 

  5. Bellissard L, De Palma N, Freyssinet A, Herrmann M, Lacourte S (1999) An agent platform for reliable asynchronous distributed programming. In: Proceedings of SRDS’99, IEEE Computer Society, pp 294–295

  6. Bergamini D, Descoubes N, Joubert C, Mateescu R (2005) BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Proceedings of TACAS’05, volume 3440 of LNCS, Springer, Berlin, pp 581–585

  7. Bernot G, Gaudel M-C, Marre B (1991) Software testing vased on formal specifications: a theory and a tool. Softw Eng J 6(6): 387–405

    Google Scholar 

  8. Boyer F, Gruber O, Salaün G (2011) Specifying and verifying the synergy reconfiguration protocol with LOTOS NT and CADP. In: Proceedings of FM’11, volume 6664 of LNCS, Springer, Berlin, pp 103–117

  9. Bozzano M, Cimatti A, Katoen J-P, Nguyen VY, Noll T, Roveri M, Wimmer R (2010) A model checker for AADL. In: Proceedings of CAV’10, volume 6174 of LNCS, Springer, Berlin, pp 562–565

  10. Cansado A, Canal C, Salaün G, Cubo J (2010) A formal framework for structural reconfiguration of components under behavioural adaptation. Electron Notes Theor Comput Sci 263:95–110

    Article  Google Scholar 

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

  12. Chapman C, Emmerich W, Galán Márquez F, Clayman S, Galis A (2010) Software architecture definition for on-demand cloud provisioning. In: Proceedings of HPDC’10, ACM Press, pp 61–72

  13. Cornejo MA, Garavel H, Mateescu R, De Palma N (2001) Specification and verification of a dynamic reconfiguration protocol for agent-based applications. In: Proceedings of DAIS’01, volume 198 of IFIP Conference Proceedings, Kluwer, pp 229–244

  14. Crouzen P, Lang F (2011) Smart reduction. In: Proceedings of FASE’11, volume 6603 of LNCS, Springer, Berlin, pp 111–126.

  15. Etchevers X, Coupaye T, Boyer F, de Palma N (2011) Self-configuration of distributed applications in the cloud. In: Proceedings of CLOUD’11, IEEE Computer Society, pp 668–675

  16. Furht B, Escalante A (eds) (2010) Handbook of cloud computing. Springer, Berlin

  17. Garavel H, Lang F, Mateescu R, Serwe W (2011) CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Proceedings of TACAS’11, volume 6605 of LNCS, Springer, Berlin, pp 372–387

  18. Garavel H, Mateescu R, Serwe W (2012) Large-scale distributed verification using CADP: beyond clusters to grids. In: Proceedings of PDMC’12

  19. Garavel H, Sighireanu M (1999) A graphical parallel composition operator for process algebras. In: Proceedings of FORTE’99, volume 156 of IFIP conference proceedings, Kluwer, pp 185–202

  20. Garavel H, Viho C, Zendri M (2001) System design of a CC-NUMA multiprocessor architecture using formal specification, model checking, co-simulation, and test generation. STTT 3(3):314–331

    MATH  Google Scholar 

  21. Goldsack P, Guijarro J, Loughran S, Coles A, Farrell A, Lain A, Murray P, Toft P (2009) The SmartFrog configuration management framework. SIGOPS Oper Syst Rev 43(1):16–25

    Article  Google Scholar 

  22. ISO/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization, Information Technology

  23. Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS Kernel. In: Proceedings of SOSP’09, ACM Press, pp 207–220

  24. Kramer J, Magee J (1990) The evolving philosophers problem: dynamic change management. IEEE TSE 16(11):1293–1306

    Google Scholar 

  25. Kramer J, Magee J (1998) Analysing dynamic change in distributed software architectures. IEE Proc Softw 145(5):146–154

    Article  Google Scholar 

  26. Krause C, Maraikar Z, Lazovik A, Arbab F (2011) Modeling dynamic reconfigurations in Reo using high-level replacement systems. Sci Comp Programm 76(1):23–36

    Article  MATH  Google Scholar 

  27. Lantreibecq E, Serwe W (2011) Model checking and co-simulation of a dynamic task dispatcher circuit using CADP. In: Proceedings of FMICS’11, volume 6959 of LNCS, Springer, pp 180–195

  28. Magee J, Kramer J, Giannakopoulou D (1999) Behaviour analysis of software architectures. In: Proceedings of WICSA’99, volume 140 of IFIP conference proceedings, Kluwer, pp 35–50

  29. Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Proceedings of FM’08, volume 5014 of LNCS, Springer, pp 148–164

  30. Mirkovic J, Faber T, Hsieh P, Malayandisamu G, Malavia R (2010) DADL: distributed application description language. USC/ISI Technical, Report ISI-TR-664

  31. Salaün G, Etchevers X, De Palma N, Boyer F, Coupaye T (2012) Verification of a self-configuration protocol for distributed applications in the cloud. In: Proceedings of SAC’12, ACM Press, pp 1278–1283

  32. Schwaber K (2004) Agile project management with scrum. Microsoft Press, Redmond

    Google Scholar 

  33. Vassev E, Hinchey M, Quigley A (2009) Model checking for autonomic systems specified with ASSL. In: Proceedings of NFM’09, pp 16–25

  34. Wermelinger M, Lopes A, Fiadeiro JL (2001) A graph based architectural (Re)configuration language. In: Proceedings of ESEC/SIGSOFT FSE’01, ACM Press, pp 21–32

Download references

Acknowledgments

The authors would like to thank Frédéric Lang and Radu Mateescu for their very interesting comments on a former version of this paper. This work has been supported by the OpenCloudware French FSN project (2012-2015).

Author information

Authors and Affiliations

  1. Grenoble INP, Inria, France

    Gwen Salaün

  2. UJF, Grenoble, France

    Fabienne Boyer, Noel De Palma & Olivier Gruber

  3. Orange Labs, Issy-les-Moulineaux, France

    Thierry Coupaye & Xavier Etchevers

Authors
  1. Gwen Salaün
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabienne Boyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thierry Coupaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Noel De Palma
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Xavier Etchevers
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Olivier Gruber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gwen Salaün.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Salaün, G., Boyer, F., Coupaye, T. et al. An experience report on the verification of autonomic protocols in the cloud. Innovations Syst Softw Eng 9, 105–117 (2013). https://doi.org/10.1007/s11334-013-0204-0

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-013-0204-0

Keywords

Search

Navigation