Skip to Main content Skip to Navigation
New interface
Conference papers

ByMC: Byzantine Model Checker

Igor Konnov 1, 2 Josef Widder 3 
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Igor Konnov Connect in order to contact the contributor
Submitted on : Wednesday, October 31, 2018 - 12:11:50 PM
Last modification on : Saturday, June 25, 2022 - 7:44:54 PM
Long-term archiving on: : Friday, February 1, 2019 - 1:47:37 PM


Files produced by the author(s)




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⟩



Record views


Files downloads