Towards scalable model checking of self-stabilizing programs

摘要

Existing approaches for verifying self-stabilization with a symbolic model checker have relied on the use of weak fairness. We point out that this approach has limited scalability. To overcome this limitation, first, we show that if self-stabilization is possible without fairness then the cost of verifying self-stabilization is substantially lower. In fact, we observe from several case studies that the cost of verification under weak fairness is more than 1000 times that of the cost without fairness.For the case where weak fairness is essential for self-stabilization, we demonstrate the feasibility of two approaches for improving scalability: (1) decomposition and (2) utilizing the weaker version of self-stabilization, namely weak stabilization. In the first approach, the designer partitions the program into components where each component satisfies its property without fairness. We show that the first approach enables us to verify Huang's mutual exclusion program for uniform rings with 31 processes (state space 10~138) whereas without this approach, it was not possible to verify the same program with 5 processes (state space 10~10). In the second approach, a weaker version of self-stabilization is verified. For Hoepman's ring-orientation program on odd-length ring, we show that it is possible to verify weak stabilization for 301 processes (state space 10~181) whereas self-stabilization could not be verified for 9 processes (state space 10~5) under weak fairness. Furthermore, one can utilize transformation algorithms to convert weak stabilizing programs to probabilistically stabilizing programs. Hence, for the case where it is not possible to verify deterministic self-stabilization, one can obtain the assurance provided by probabilistic self-stabilization at a significantly reduced cost. Finally, we also present 5 case studies to illustrate the scalability of stabilization with techniques suggested in this paper.