Specification-Based Design of Self-Stabilization

Research in system stabilization has traditionally relied on the availability of a complete system implementation. As such, it would appear that the scalability and reusability of stabilization is limited in practice. To redress this perception, in this paper, we show for the first time that system stabilization may be designed knowing only the system specification but not the system implementation. We refer to stabilization designed thus as
specification-based design of stabilization
and identify “local everywhere specifications” and “convergence refinements” as being amenable to the specification-based design of stabilization. Using our approach, we present the design of Dijkstra’s four-state stabilizing token-ring system starting from an abstract fault-intolerant token-ring system. We also present an illustration of automated design of specification-based stabilization on a three-state token-ring system.