Specification-Based Design of Self-Stabilization
Murat Demirbaş, Anish Arora · IEEE Transactions on Parallel and Distributed Systems · 2015
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.