A Verification Technique for Self-Stabilizing Algorithms based on Ljapunov's
``Second Method''
Oliver Theel
To appear at Nineteenth Annual
ACM SIGACT-SIGOPS Symposium on PRINCIPLES OF DISTRIBUTED COMPUTING (PODC
2000), Portland, Oregon, 16-19 July 2000
Abstract
A particularly suitable design strategy for constructing a robust distributed
algorithm is to endow it with a self-stabilization property. Such a property
guarantees that the system will always return to and stay within a specified
set of legal states within bounded time regardless of its initial state.
A self-stabilizing application therefore has the potential of recovering
from the effects of arbitrary transient failures. However, to actually
verify that an application self-stabilizes can be quite tedious with current
proof methodologies and is non-trivial. The self-stabilizing property of
distributed algorithms exhibits interesting analogies to stabilizing control
circuits used in various engineering domains. In this brief announcement
we would like to draw attention to the fact that methodologies from control
theory, namely Ljapunov's ``Second Method'' can be used to more easily
verify the self-stabilization property of distributed algorithms.