Compositional Proofs of Self-stabilizing Protocols
George M. Varghese · McGill-Queen's University Press eBooks · 1997
We describe a modularity theorem for self-stabilizing protocols. The theorem shows that self-stabilizing component automata (that possess a property called suffix closure) can be composed to form a self-stabilizing system. Our theorem is more general than prior compositional theorems, and is described using the timed 110 automaton model to facilitate the proof of stabilization time bounds. We also use a simple theorem that facilitates hierarchical proofs for stabilizing protocols. Taken together, the theorems for compositional and hierarchical proofs allow the verification of of complex self-stabilizing systems. We describe example applications.