Towards scalable model checking of self-stabilizing programs

Jingshu Chen, Fuad Abujarad and Sandeep S. Kulkarni


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 cost of verifying self-stabilization is substantially lower. In fact, we observe from several case studies that 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 {\em weak stabilization}. In the first approach, 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.


Return to the publication list
Return to the Sandeep's home page