ByMC: Byzantine Model Checker

Igor Konnov 1 Josef Widder 2
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
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 metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01909653
Contributor : Igor Konnov <>
Submitted on : Wednesday, October 31, 2018 - 12:11:50 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Friday, February 1, 2019 - 1:47:37 PM

File

camera.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

516

Files downloads

179