University of Waterloo (CANADA)
CADP (Construction and Analysis of Distributed Processes)
2,456,936 states and 59,409,357 transitions
Construction of correct distributed systems is a challenge and prone to
error, not least because the design and implemetation of distributed
algorithms must take into account their complexity, concurrency, and
non-determinism and must allow for unexpected physical and external
events such as faults. This case study presents an example of how to
apply component-based modeling, verification, and performance
evaluation of a self-stabilizing systems based on the BIP framework,
applied to a distributed reset algorithm.
Distributed reset was modeled using the BIP language and framework, by creating the components in the tree layer and wave layer and composing them, together with cross-layer interactions, to build the distributed reset. To model check this, the BIP state-space explorer was used to construct a finite representation as a Labeled Transition System (LTS). Using the EVALUATOR model checker of CADP, a number of temporal logic formulas representing key correctness properties (closure, deadlock-freedom, and finite reachability) were successfully verified on the LTS of the distributed reset algorithm.
This case study demonstrates the successful application of a method for
integrating high-level modeling with verification of functional
properties of a distributed system, by combining the BIP framework and
the CADP toolbox.
Ananda Basu, Borzoo Bonakdarpour, Marius Bozga, and Joseph Sifakis.
"Systematic Correct Construction of Self-stabilizing Systems: A Case
Study". Proceedings of the 12th International Symposium on
Stabilization, Safety, and Security of Distributed Systems SSS'10,
Lecture Notes in Computer Science vol. 6366, pages 4-18. Springer
Verlag, September 2010.
Available on-line at: http://www.springerlink.com/content/d6k4k4824r474577/
or from our FTP site in PDF PostScript
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
CANADA N2L 3G1
This case study, amongst others, is described on the CADP Web site: