Formalism of self-stabilization with linear temporal logic and its verification

The last several decades have seen a rapid growth of information technology. Distributed systems are used world-wide in our daily life. Clearly, the correctness of such systems is of crucial importance. Failures of those systems can be potentially disastrous and cause huge amount of money. One way to guarantee that these systems tolerate transient faults is done by making them self-stabilizing systems, which automatically recover from any transient fault. Mathematics can provide solid foundations for methods to describe and analyze systems. Formal methods are of this kind. Moreover, formal analysis techniques can be used to verify whether a system has desired properties. In this paper, we present a formalism of self-stabilization concept based on Linear Temporal Logic (LTL), and apply the model checking as formal verification of the formalism.