INRIA Rhône-Alpes, Grenoble
University Joseph Fourier, Grenoble
Grenoble INP (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
3700 lines of LNT (data types, functions, and processes).
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
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.
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.
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 our FTP site in PDF or PostScript
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 54 28
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|