Abstract
Dynamic software systems that provide the ability to reconfigure themselves seem to be reaching a complexity that suggests the use of formal methods in the design process, helping system designers master that complexity, better understand their systems, find and correct bugs rapidly, and ultimately build strong confidence in the correctness of their systems. As an illustration of this trend, this paper reports on our experience with the co-design and specification of the reconfiguration protocol of a component-based platform, intended as the foundation for building robust dynamic systems. We wrote the specification in Lotos NT, whose evolution from the E-Lotos standard proved especially suited to this work. We extensively verified the protocol using the Cadp toolbox. This formal analysis helped to detect several issues which enabled us to correct various parts of the protocol. The protocol is implemented in the Synergy virtual machine, the prototype of an ongoing research programme on reconfigurable and robust component-aware virtual machines.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
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)
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)
Bruneton, É., Coupaye, T., Leclercq, M., Quéma, V., Stefani, J.B.: The Fractal Component Model and its Support in Java. Software – Practice and Experience 36(11-12), 1257–1284 (2006)
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.1). INRIA/VASY, 109 pages (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, Dordrecht (2001)
Coulson, G., Blair, G., Clarke, M., Parlavantzas, N.: The Design of a Configurable and Reconfigurable Middleware Platform. Distributed Computing 15(2), 109–126 (2002)
Coulson, G., Blair, G., Grace, P., Taiani, F., Joolia, A., Lee, K., Ueyama, J., Sivaharan, T.: A Generic Component Model for Building Systems Software. ACM Trans. Comput. Syst. 26(1), 1–42 (2008)
David, P.-C., Ledoux, T.: An Aspect-Oriented Approach for Developing Self-Adaptive Fractal Components. In: Löwe, W., Südholt, M. (eds.) SC 2006. LNCS, vol. 4089, pp. 82–97. Springer, Heidelberg (2006)
Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
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, New York (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)
Krause, C., Maraikar, Z., Lazovik, A., Arbab, F.: Modeling Dynamic Reconfigurations in Reo using High-level Replacement Systems. Science of Computer Programming 76(1), 23–36 (2011)
Kulkarni, S.S., Biyani, K.N.: Correctness of Component-Based Adaptation. In: Crnković, I., Stafford, J.A., Schmidt, H.W., Wallnau, K. (eds.) CBSE 2004. LNCS, vol. 3054, pp. 48–58. Springer, Heidelberg (2004)
Léger, M., Ledoux, T., Coupaye, T.: Reliable Dynamic Reconfigurations in a Reflective Component Model. In: Grunske, L., Reussner, R., Plasil, F. (eds.) CBSE 2010. LNCS, vol. 6092, pp. 74–92. Springer, Heidelberg (2010)
Magee, J., Kramer, J.: Dynamic Structure in Software Architectures. In: SIGSOFT FSE 1996, pp. 3–14. ACM, New York (1996)
Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Science of Computer Programming 46(3), 255–281 (2003)
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, New York (2001)
Zhang, J., Cheng, B.H.C.: Model-based Development of Dynamically Adaptive Software. In: Proc. of ICSE 2006, pp. 371–380. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boyer, F., Gruber, O., Salaün, G. (2011). Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-21437-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21436-3
Online ISBN: 978-3-642-21437-0
eBook Packages: Computer ScienceComputer Science (R0)