[Back]

M. Lazić, I. Konnov, H. Veith, J. Widder:
"Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms";
Talk: 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia (invited); 2016-07-14 - 2016-07-15.

Critical distributed systems are designed to tolerate faults of individual components; they must work even if some of their components fail. Model checking of fault-tolerant distributed algorithms is challenging: the algorithms have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm code is parameterized due to conditions involving counting the number of received messages (thresholds). We present our framework that allows us both, modeling distributed algorithms adequately and model checking them efficiently. To address parameterization, we introduced several abstraction and partial order reduction techniques. As a result, we verified several fault-tolerant broadcast and agreement algorithms for all system sizes and all possible numbers of faults.

model checking, fault tolerance, parameterized verification

Project Head Igor Konnov:
Abstraction-based Parameterized TLA Checker

Project Head Josef Widder:
Parametrized Verification of Fault-tolerant Distributed Algorithms