A strategy for automatic verification of stabilization of distributed algorithms

Ritwika Ghosh, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 link-reversal, shortest path computation, distributed coloring, leader election and spanning-tree construction.

Original languageEnglish (US)
Title of host publicationFormal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015 Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Proceedings
EditorsMahesh Viswanathan, Susanne Graf
PublisherSpringer
Pages35-49
Number of pages15
ISBN (Print)9783319191942
DOIs
StatePublished - 2015
Event35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2015 Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015 - Grenoble, France
Duration: Jun 2 2015Jun 4 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9039
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2015 Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015
Country/TerritoryFrance
CityGrenoble
Period6/2/156/4/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A strategy for automatic verification of stabilization of distributed algorithms'. Together they form a unique fingerprint.

Cite this