An automatic approach to self-stabilization

We present a formal method to design self-stabilizing algorithms by using graph rewriting systems (GRS). This method is based on two phases. The first phase consists of defining the set of illegitimate configurations (GRSIC). The second phase allows to construct some local correction rules to eliminate the illegitimate configurations. Then the graph relabeling system composed of the initial graph rewriting system improved with the addition of the correction rules is a self-stabilizing system (LSGRS). We obtain a general approach to deal with fault-tolerance in distributed computing. We illustrate our approach by various self-stabilizing algorithms for computing distributed spanning trees and SSP´s algorithm.