ByMC: Byzantine Model Checker

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.
Type de document :
Communication dans un congrès
ISoLA 2018 - 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2018, Limassol, Cyprus. 11246, pp.327-342, 2018, Lecture Notes in Computer Science. 〈http://www.isola-conference.org/isola2018/〉. 〈10.1007/978-3-030-03424-5_22〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01909653
Contributeur : Igor Konnov <>
Soumis le : mercredi 31 octobre 2018 - 12:11:50
Dernière modification le : vendredi 9 novembre 2018 - 10:44:00

Fichier

camera.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 11246, pp.327-342, 2018, Lecture Notes in Computer Science. 〈http://www.isola-conference.org/isola2018/〉. 〈10.1007/978-3-030-03424-5_22〉. 〈hal-01909653〉

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

41