Synthesis of a simple self-stabilizing system

TL;DR

This paper presents a straightforward template-based method for designing self-stabilizing distributed systems using bounded model checking, aiming to enhance systematic and automated system synthesis.

Contribution

It introduces a novel approach combining template-based design with bounded model checking for the synthesis of self-stabilizing distributed systems.

Findings

Demonstrates the feasibility of the approach on classical examples

Provides a systematic method for distributed system synthesis

Enhances automation in designing self-stabilizing systems

Abstract

With the increasing importance of distributed systems as a computing paradigm, a systematic approach to their design is needed. Although the area of formal verification has made enormous advances towards this goal, the resulting functionalities are limited to detecting problems in a particular design. By means of a classical example, we illustrate a simple template-based approach to computer-aided design of distributed systems based on leveraging the well-known technique of bounded model checking to the synthesis setting.