Lightweight Methods for Automated Design of Self-Stabilization

Software systems are an integral part of almost every modern piece of technology. In complex inter-networked systems, software dependability issues are of a major concern, especially robustness to transient faults. The Self-Stabilization (SS) property guarantees that a system will regain its normal behavior in a finite amount of time when faults stop occurring, and will maintain its normal execution as long as there are no faults. SS is a desirable property of robust network protocols, however, it is intellectually challenging to manually design and verify SS. In this paper, we propose a new vision for automated design and verification of SS. Specifically, our approach puts forward a paradigm of {em synthesize-in-small-scale} and {em generalize}. We automatically synthesize SS for small instances of non-stabilizing protocols and provide techniques that help designers in generalizing these small solutions for larger instances of the synthesized protocols. Our preliminary results are promising as we have automatically generated self-stabilizing protocols that are the same as their manually designed versions, and alternative solutions for well known problems. We also discuss our plans for future work.