ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 11:00 - 11:40 at S510 - Behavioural models and parametrised systems Chair(s): Tiziana Margaria

Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. The combination of these challenges makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where no process enters round r before all other processes finished round r − 1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework to classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Behavioural models and parametrised systemsMeTRiD at S510
Chair(s): Tiziana Margaria University of Limerick and Lero - The Irish Software Research Centre
11:00
40m
Talk
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
MeTRiD
Nathalie Bertrand INRIA Rennes, Igor Konnov Inria Nancy, Marijana Lazić TU Wien, Josef Widder TU Wien
11:40
40m
Talk
Revisiting the Glue of BIP
MeTRiD
Jacques Combaz Verimag/CNRS
12:20
40m
Talk
Programming Dynamic Reconfigurable Systems with DR-BIP
MeTRiD
Rim El Ballouli Verimag, Saddek Bensalem Verimag, Marius Bozga Verimag/CNRS, Joseph Sifakis Verimag/CNRS