Formal design of self-stabilizing programs

Abstract

Experience has shown that reasoning informally about distributed algorithms is extremely dangerous and error-prone, although the underlying method of reasoning is appealing. On the other hand, completely formal proofs of even simple algorithms are tedious to construct and dicult to follow. In this paper we propose a number of new operators for the UNITY logic, which enable us to reason completely formal about self-stabilizing algorithms, while maintaining the structures which play a role in the development of the algorithm. The paper includes some examples in which we show how various laws are used, and how design strategies can be represented in formal structures.