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 the CADP Web 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: www-cadp:/case-studies

Back to the CADP case studies page