Symbolic model checking for self-stabilizing algorithms

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our resul ts of using symbolic model checking to verify distributed algorithms agains t the self-stabilizing property. In general, the most difficult problem wit h model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all pos sible initial states. So far applying model checking to self-stabilizing al gorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checkin g for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advanta ge that most of its computations do not depend on the initial states. We sh ow how to verify the correctness of algorithms by means of SMV, a well-know n symbolic model checker. By applying the proposed approach to several algo rithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently . Through these case studies, we also demonstrate the usefulness of the pro posed approach in detecting errors.