%0 Conference Proceedings
%T A Strategy for Automatic Verification of Stabilization of Distributed Algorithms
%+ University of Illinois at Urbana-Champaign [Urbana] (UIUC)
%A Ghosh, Ritwika
%A Mitra, Sayan
%Z Part 1: Ensuring Properties of Distributed Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 35-49
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_3
%K Measure Function
%K Model Check
%K Transition System
%K Interaction Graph
%K Small Model
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767335/document
%2 https://inria.hal.science/hal-01767335/file/978-3-319-19195-9_3_Chapter.pdf
%L hal-01767335
%U https://inria.hal.science/hal-01767335
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039