Specifying and verifying the SYNERGY reconfiguration protocol with LOTOS NT and CADP

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. © 2011 Springer-Verlag.