Formally Proving and Enhancing a Self-Stabilising Distributed Algorithm

TL;DR

This paper demonstrates how formal modelling and verification techniques can prove correctness, stability, and additional properties of a distributed algorithm that transforms a tree into a ring topology.

Contribution

It introduces a formal Coloured Petri net model for a self-stabilising algorithm, enabling proof of correctness, stability, and new properties, and suggests simplifications.

Findings

Proved the algorithm's correctness and self-stabilising nature.

Showed the algorithm's termination and silentness properties.

Identified simplifications without losing generality.

Abstract

This paper presents the benefits of formal modelling and verification techniques for self-stabilising distributed algorithms. An algorithm is studied, that takes a set of processes connected by a tree topology and converts it to a ring configuration. The Coloured Petri net model not only facilitates the proof that the algorithm is correct and self-stabilising but also easily shows that it enjoys new properties of termination and silentness. Further, the formal results show how the algorithm can be simplified without loss of generality.