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

Fabienne Boyer, Olivier Gruber, and Gwen Salaün

Proceedings of the 17th International Symposium on Formal Methods FM'11 (Limerick, Ireland), June 2011

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.

15 pages

PDF

PostScript

Slides of G. Salaün's lecture at FM'11

PDF