Systematic Correct Construction of Self-stabilizing Systems: A Case Study

Design and implementation of distributed algorithms often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We present a methodology for component-based modeling, verification, and performance evaluation of self-stabilizing systems based on the BIP framework. In BIP, a system is modeled as the composition of a set of atomic components by using two types of operators: interactions describing synchronization constraints between components, and priorities to specify scheduling constraints. The methodology involves three steps illustrated using the distributed reset algorithm due to Arora and Gouda. First, a high-level model of the algorithm is built in BIP from the set of its processes by using powerful primitives for multi-party interactions and scheduling. Then, we u...

• Type: Journal
• Year: 2010
• Where: SSS
• Authors: Ananda Basu, Borzoo Bonakdarpour, Marius Bozga, Joseph Sifakis
• Keywords: Algorithm, Control Systems, Correct Distributed Systems, Model, SSS 2010