Formal design of self-stabilizing programs: Theory and examples

Abstract

It is commonly realized that informal reasoning about distributed algorithms in general and self-stabilizing systems in particular is very error-prone. Formal method is considered as a promising solution, but is still in an immature state for the fact that formal proofs of even simple algorithms are tedious and difficult to follow. We believe that to make the method more appealing one should not only pay attention to 'theoretical' issues such as consistency and completeness, but also to the 'ergonomics' of the method. In this spirit, this paper proposes a number of new operators to model self-stabilization and a formalization of a number of useful design strategies. It is hoped that their use can improve the ease with which algorithmic reasoning is formally applied. Some examples showing how various laws are used will given in Part II.