Igor Konnov: Model Checking of Threshold-based Fault-tolerant Distributed Algorithms

[Pozor: dobimo se v sredo, 4. 6. 2016 od 10h do 12h.]

Model Checking of Threshold-based Fault-tolerant Distributed Algorithms

Igor Konnov, Technische Univesrität Wien

Abstract: 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 algorithm 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.

This talk is based on joint work with Annu Gmeiner, Ulrich Schmid, Helmut Veith, and Josef Widder.

Bio: Dr. Igor Konnov is a postdoc at the Formal Methods in Systems Engineering Group, TU Wien (Vienna University of Technology) since 2011. He received his PhD and Specialist (comparable to MSc) degrees in Applied Mathematics from Lomonosov Moscow State University. His research interests include model checking, parameterized model checking, and verification of distributed algorithms.