Database of Case Studies Achieved Using CADP

Systematic Correct Construction of Self-Stabilizing Systems

Organisation: University of Waterloo (CANADA)
VERIMAG (FRANCE)

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: http://www.springerlink.com/content/d6k4k4824r474577/
or from our FTP site in PDF PostScript
Contact:
Borzoo Bonakdarpour
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario
CANADA N2L 3G1
Email: borzoo@ecemail.uwaterloo.ca

Further remarks:
This case study, amongst others, is described on the CADP Web site:
http://cadp.inria.fr/case-studies


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


Back to the CADP case studies page