ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 14:30 - 15:00 at SUN I - Safety and Fault-tolerant Systems Chair(s): Rance Cleaveland

Owing to well-known limitations of what can be achieved in purely asynchronous systems, 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.

Thu 11 Apr

tacas-2019-papers
14:00 - 16:00: TACAS 2019 - Safety and Fault-tolerant Systems at SUN I
Chair(s): Rance CleavelandUniversity of Maryland
tacas-2019-papers14:00 - 14:30
Talk
Link to publication
tacas-2019-papers14:30 - 15:00
Talk
Ilina StoilkovskaVienna University of Technology , Igor KonnovInria Nancy, Josef WidderTU Wien, Florian ZulegerVienna University of Technology
Link to publication
tacas-2019-papers15:00 - 15:30
Talk
Pablo CastroDept. of Computer Science FCEFQyN, University of Rio Cuarto, Pedro D'Argenio, Ramiro Demasi, Luciano Putruele
Link to publication
tacas-2019-papers15:30 - 16:00
Talk
Philipp Dominik SchubertHeinz Nixdorf Institut, Paderborn University, Ben HermannUniversity of Paderborn, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication