ByMC: Byzantine Model Checker

Igor Konnov (1, 2) , Josef Widder (3)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 MOSEL - Proof-oriented development of computer-based systems
3 Institut für Informationssysteme [Wien]

In recent work [12,10], we have introduced a technique for automatic verification of threshold-guarded distributed algorithms that have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and progress when they receive sufficiently many messages, e.g., at least t + 1; (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., n > 3t. In this paper, we present Byzantine Model Checker that implements the above-mentioned technique. It takes two kinds of inputs, namely, (i) threshold automata (the framework of our verification techniques) or (ii) Parametric Promela (which is similar to the way in which the distributed algorithms were described in the literature). We introduce a parallel extension of the tool, which exploits the parallelism enabled by our technique on an MPI cluster. We compare performance of the original technique and of the extensions by verifying 10 benchmarks that model fault-tolerant distributed algorithms from the literature. For each benchmark algorithm we check two encodings: a manual encoding in threshold automata vs. a Promela encoding.

Mots clés: model checking; fault tolerance; distributed algorithms

Domaines: Génie logiciel [cs.SE]; Calcul parallèle, distribué et partagé [cs.DC]; Logique en informatique [cs.LO]

Igor Konnov, Josef Widder. ByMC: Byzantine Model Checker. ISoLA 2018 - 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2018, Limassol, Cyprus. pp.327-342, ⟨10.1007/978-3-030-03424-5_22⟩. ⟨hal-01909653⟩