Skip to Main content Skip to Navigation
New interface
Conference papers

A Strategy for Automatic Verification of Stabilization of Distributed Algorithms

Abstract : Automatic verification of convergence and stabilization properties of distributed algorithms has received less attention than verification of invariance properties. We present a semi-automatic strategy for verification of stabilization properties of arbitrarily large networks under structural and fairness constraints. We introduce a sufficient condition that guarantees that every fair execution of any (arbitrarily large) instance of the system stabilizes to the target set of states. In addition to specifying the protocol executed by each agent in the network and the stabilizing set, the user also has to provide a measure function or a ranking function. With this, we show that for a restricted but useful class of distributed algorithms, the sufficient condition can be automatically checked for arbitrarily large networks, by exploiting the small model properties of these conditions. We illustrate the method by automatically verifying several well-known distributed algorithms including linkreversal, shortest path computation, distributed coloring, leader election and spanning-tree construction.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 10:19:08 AM
Last modification on : Thursday, August 1, 2019 - 2:12:06 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Ritwika Ghosh, Sayan Mitra. A Strategy for Automatic Verification of Stabilization of Distributed Algorithms. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.35-49, ⟨10.1007/978-3-319-19195-9_3⟩. ⟨hal-01767335⟩



Record views


Files downloads