Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
| Autor: | Florian Zuleger, Josef Widder, Ilina Stoilkovska, Igor Konnov |
|---|---|
| Přispěvatelé: | Vienna University of Technology (TU Wien), Institut für Informationssysteme [Wien], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Model checking
Theoretical computer science Semantics (computer science) Reachability problem Computer science Parameterized complexity [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 0102 computer and information sciences 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] 01 natural sciences Undecidable problem Distributed algorithm 010201 computation theory & mathematics Bounded function Theory of computation 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] Computer Science::Formal Languages and Automata Theory Software Information Systems |
| Zdroj: | TACAS 2019-International Conference on Tools and Algorithms for the Construction and Analysis of Systems 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⟩ Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030174644 TACAS (2) |
| DOI: | 10.1007/978-3-030-17465-1_20⟩ |
| Popis: | International audience; 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|