Skip to Main content Skip to Navigation
Conference papers

Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking

Ilina Stoilkovska 1, 2 Igor Konnov 3, 4 Josef Widder 1, 2 Florian Zuleger 1, 2
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Many fault-tolerant distributed algorithms are designed for synchronous or round-based semantics. In this paper, we introduce the synchronous variant of threshold automata, and study their applicability and limitations for the verification of synchronous distributed algorithms. We show that in general, the reachability problem is undecidable for synchronous threshold automata. Still, we show that many synchronous fault-tolerant distributed algorithms have a bounded diameter, although the algorithms are parameterized by the number of processes. Hence, we use bounded model checking for verifying these algorithms. The existence of bounded diameters is the main conceptual insight in this paper. We compute the diameter of several algorithms and check their safety properties, using SMT queries that contain quantifiers for dealing with the parameters symbolically. Surprisingly, performance of the SMT solvers on these queries is very good, reflecting the recent progress in dealing with quantified queries. We found that the diameter bounds of synchronous algorithms in the literature are tiny (from 1 to 4), which makes our approach applicable in practice. For a specific class of algorithms we also establish a theoretical result on the existence of a diameter, providing a first explanation for our experimental results. The encodings of our benchmarks and instructions on how to run the experiments are available at: [33].
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Igor Konnov Connect in order to contact the contributor
Submitted on : Friday, October 11, 2019 - 6:08:27 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:13 AM


Files produced by the author(s)




Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger. Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. TACAS 2019 - International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17465-1_20⟩. ⟨hal-01925653v2⟩



Les métriques sont temporairement indisponibles