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.
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.