Database of Case Studies Achieved Using CADP

Systematic Correct Construction of Self-Stabilizing Systems

Organisation: University of Waterloo (CANADA)

Method: BIP

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed Systems.

Period: 2010

Size: 2,456,936 states and 59,409,357 transitions

Description: 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.

Conclusions: 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.

Publications: [Basu-Bonakdarpour-Bozga-Sifakis-10] 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:
or from our FTP site in PDF PostScript
Borzoo Bonakdarpour
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario

Further remarks:
This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page