Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS-NT and CADP

Fabienne Boyer (1) , Olivier Gruber (1) , Gwen Salaün (2, 3)

1 UJF - Université Joseph Fourier - Grenoble 1
2 Grenoble INP - Institut polytechnique de Grenoble - Grenoble Institute of Technology
3 VASY - System validation - Research and applications

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.

Domaines: Génie logiciel [cs.SE]

Fabienne Boyer, Olivier Gruber, Gwen Salaün. Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS-NT and CADP. 17th International Symposium on Formal Methods (FM'11), Jun 2011, Limerick, Ireland. pp.103-117, ⟨10.1007/978-3-642-21437-0_10⟩. ⟨hal-00648909⟩