Abstract
Distributed applications in the cloud are composed of a set of virtual machines running a set of interconnected software components. In this context, setting up, (re)configuring, and monitoring these applications is a real burden since 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. In this paper, we focus on 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Open Virtualization Format Specification. Specification 1.1.0, Distributed Management Task Force DMTF Standard (2010)
Allen, R.B., Douence, R., Garlan, D.: Specifying and Analyzing Dynamic Software Architectures. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998)
Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural Models for Distributed Fractal Components. Annales des Télécommunications 64(1-2), 25–43 (2009)
Bellissard, L., De Palma, N., Freyssinet, A., Herrmann, M., Lacourte, S.: An Agent Platform for Reliable Asynchronous Distributed Programming. In: Proc. of SRDS 1999, pp. 294–295. IEEE Computer Society (1999)
Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 581–585. Springer, Heidelberg (2005)
Boyer, F., Gruber, O., Salaün, G.: Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 103–117. Springer, Heidelberg (2011)
Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M., Wimmer, R.: A Model Checker for AADL. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 562–565. Springer, Heidelberg (2010)
Broto, L., Hagimont, D., Stolf, P., De Palma, N., Temate, S.: Autonomic Management Policy Specification in Tune. In: Proc. of SAC 2008, pp. 1658–1663. ACM (2008)
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA/VASY (2011)
Chapman, C., Emmerich, W., Galán Márquez, F., Clayman, S., Galis, A.: Software Architecture Definition for On-demand Cloud Provisioning. In: Proc. of HPDC 2010, pp. 61–72. ACM Press (2010)
Cornejo, M.A., Garavel, H., Mateescu, R., De Palma, N.: Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. In: Proc. of DAIS 2001. IFIP Conference Proceedings, vol. 198, pp. 229–244. Kluwer (2001)
Dillenseger, B.: CLIF, a Framework based on Fractal for Flexible, Distributed Load Testing. Annales des Télécommunications 64(1-2), 101–120 (2009)
Etchevers, X., Coupaye, T., Boyer, F., de Palma, N.: Self-Configuration of Distributed Applications in the Cloud. In: Proc. of CLOUD 2011, pp. 668–675. IEEE Computer Society (2011)
Etchevers, X., Coupaye, T., Boyer, F., de Palma, N., Salaün, G.: Automated Configuration of Legacy Applications in the Cloud. In: Proc. of UCC 2011, pp. 170–177. IEEE Computer Society (2011)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Goldsack, P., Guijarro, J., Loughran, S., Coles, A., Farrell, A., Lain, A., Murray, P., Toft, P.: The SmartFrog Configuration Management Framework. SIGOPS Oper. Syst. Rev. 43(1), 16–25 (2009)
Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., Van Weerdenburg, M.: The Formal Specification Language mCRL2. In: Dagstuhl Seminars (2007)
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization — Information Technology (2001)
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.: seL4: Formal Verification of an OS Kernel. In: Proc. of SOSP 2009, pp. 207–220. ACM Press (2009)
Kramer, J., Magee, J.: The Evolving Philosophers Problem: Dynamic Change Management. IEEE TSE 16(11), 1293–1306 (1990)
Kramer, J., Magee, J.: Analysing Dynamic Change in Distributed Software Architectures. IEE Proceedings - Software 145(5), 146–154 (1998)
Magee, J., Kramer, J., Giannakopoulou, D.: Behaviour Analysis of Software Architectures. In: Proc. of WICSA 1999. IFIP Conference Proceedings, vol. 140, pp. 35–50. Kluwer (1999)
Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Mirkovic, J., Faber, T., Hsieh, P., Malayandisamu, G., Malavia, R.: DADL: Distributed Application Description Language. USC/ISI Technical Report ISI-TR-664 (2010)
Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
Salaün, G., Etchevers, X., De Palma, N., Boyer, F., Coupaye, T.: Verification of a Self-configuration Protocol for Distributed Applications in the Cloud. In: Proc. of SAC 2012, pp. 1278–1283. ACM Press (2012)
Vassev, E., Hinchey, M., Quigley, A.: Model Checking for Autonomic Systems Specified with ASSL. In: Proc. of NFM 2009, pp. 16–25 (2009)
Wermelinger, M., Lopes, A., Fiadeiro, J.L.: A Graph Based Architectural (Re)configuration Language. In: Proc. of ESEC / SIGSOFT FSE 2001, pp. 21–32. ACM Press (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Salaün, G., Etchevers, X., De Palma, N., Boyer, F., Coupaye, T. (2013). Verification of a Self-configuration Protocol for Distributed Applications in the Cloud. In: Cámara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds) Assurances for Self-Adaptive Systems. Lecture Notes in Computer Science, vol 7740. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36249-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-36249-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36248-4
Online ISBN: 978-3-642-36249-1
eBook Packages: Computer ScienceComputer Science (R0)