Abstract
Cloud applications are composed of a set of interconnected software components distributed over several virtual machines. There is a need for protocols that can dynamically reconfigure such distributed applications. In this paper, we present a novel protocol, which is able to resolve dependencies in these applications, by (dis)connecting and starting/stopping components in a specific order. These virtual machines interact through a publish-subscribe communication media and reconfigure themselves upon demand in a decentralised fashion. Designing such protocols is an error-prone task. Therefore, we decided to specify the protocol with the LNT value-passing process algebra and to verify it using the model checking tools available in the CADP toolbox. As a result, the introduction of formal techniques and tools help to deeply revise the protocol, and these improvements have been taken into account in the corresponding Java implementation.
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.
Similar content being viewed by others
References
Allen, R., 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)
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)
Cansado, A., Canal, C., Salaün, G., Cubo, J.: A Formal Framework for Structural Reconfiguration of Components under Behavioural Adaptation. Electr. Notes Theor. Comput. Sci. 263, 95–110 (2010)
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)
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)
Fischer, J., Majumdar, R., Esmaeilsabzali, S.: Engage: A Deployment Management System. In: Proc. of PLDI 2012, pp. 263–274. ACM (2012)
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)
ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization — Information Processing Systems — Open Systems Interconnection (1989)
Kramer, J., Magee, J.: Analysing Dynamic Change in Distributed Software Architectures. IEE Proceedings - Software 145(5), 146–154 (1998)
Magee, J., Kramer, J.: Dynamic Structure in Software Architectures. In: Proc. of SIGSOFT FSE 1996, pp. 3–14. ACM (1996)
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)
Salaün, G.: Generation of Service Wrapper Protocols from Choreography Specifications. In: Proc. of SEFM 2008, pp. 313–322. IEEE Computer Society (2008)
Salaün, G., Boyer, F., Coupaye, T., De Palma, N., Etchevers, X., Gruber, O.: An Experience Report on the Verification of Autonomic Protocols in the Cloud. ISSE 9(2), 105–117 (2013)
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)
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 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Abid, R., Salaün, G., Bongiovanni, F., De Palma, N. (2013). Verification of a Dynamic Management Protocol for Cloud Applications. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)