SYNERGY Reconfiguration Protocol

Organisation:	INRIA Rhône-Alpes, Grenoble University Joseph Fourier, Grenoble Grenoble INP (FRANCE)
Method:	LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Algorithms.
Period:	2011
Size:	3700 lines of LNT (data types, functions, and processes).
Description:	A major factor in the complexity of modern software systems is their ability to reconfigure themselves as required by changing circumstances. This ability often relies on the component paradigm where software is understood as an assembly of components that can be reconfigured dynamically as one sees fit. While expressing a desired reconfiguration is relatively simple, actually evolving a running system, without shutting it down, is complex. This is even more complex when considering failures that may happen during the reconfiguration process. At the heart of this reconfiguration capability lies the reconfiguration protocol, which is responsible for incrementally and correctly evolving a running system. A key challenge of this protocol is to compute and order the set of individual reconfiguration operations that are necessary to evolve one assembly of components into another. This case-study deals with a dynamic reconfiguration protocol designed and implemented in the SYNERGY virtual machine, an experimental JAVA virtual machine that is fully component-aware and strives to guarantee robust software reconfigurations. Soon after a first version was partially running, it became obvious that the complexity of the protocol required a more formal approach, relying on specifying and verifying the protocol to help not only the design and implementation efforts but also increase the confidence of the overall robustness of the protocol. The reconfiguration protocol was formally specified in LNT and analyzed with CADP. Three facets of the protocol were verified: structural invariants, reconfiguration grammars, and temporal properties. Invariants were checked by means of functions that traverse the data terms storing the assemblies being reconfigured, and return Boolean values. These values are visible in the LTS as parameters of specific actions, and are checked using a simple invariant property that all these actions appearing in the state space never contain a wrong value. Fourteen further temporal properties were identified, formulated in modal mu-calculus, and verified using the EVALUATOR model checker of CADP. Reconfiguration grammars ensure that components respect the correct ordering of actions throughout the protocol. For each component involved in a system under reconfiguration, it was verified that its grammar is never violated. This is checked using first hiding and reduction techniques on the whole state space to keep only operations corresponding to that component. Then, it is checked that the resulting LTS is branching equivalent to the grammar using the BISIMULATOR equivalence checker. Experiments were conducted on more than 200 hand-crafted examples of current and target assemblies, characterized by the number of components, the maximum number of wires, and the number of reconfigurations necessary to evolve the current assembly into the target one.
Conclusions:	LNT has a user-friendly syntax and supports the description of complex data types written using a functional specification language. This makes specifications easy to understand and write by system designers. For this case-study, this greatly simplified the design and analysis process. This reduced gap between the specification and the real implementation of the system drastically improved the confidence of system experts in the relevance of the verification process. Moreover, the late introduction of formal techniques and the establishment of a virtuous circle between the design, the specification, the verification, and the implementation efforts, were a success. It lowered the entry costs for specification specialists because the specification could be approached incrementally, in parallel with the design and implementation of the real system. It also helped the understanding of the finer points of the protocol earlier, thereby significantly reducing the implementation and testing efforts.
Publications:	[Boyer-Gruber-Salaun-11] Fabienne Boyer, Olivier Gruber, and Gwen Salaün. "Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP". Proceedings of the 17th International Symposium on Formal Methods FM'2011 (Limerick, Ireland), Lecture Notes in Computer Science vol. 6664, pages 103-117. Springer Verlag, June 2011. Available on-line from http://cadp.inria.fr/publications/Boyer-Gruber-Salaun-11.html and from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün INRIA Rhône-Alpes / VASY 655, avenue de l'Europe F-38330 Montbonnot Saint Martin France Tel: +33 (0)4 76 61 54 28 Fax: +33 (0)4 76 61 52 52 Email: Gwen.Salaun@inria.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page