Title: Tutorial: Parameterized Verification with Byzantine Model Checker
Authors: Konnov, Igor 
Lazic, Marijana 
Stoilkovska, Ilina 
Widder, Josef 
Keywords: distributed systems; fault tolerance; parameterized model checking
Issue Date: 8-Jun-2020
Book Title: Formal Techniques for Distributed Objects, Components, and Systems. 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings 
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems of distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as Tendermint consensus. In this tutorial, we give an overview of the techniques implemented in Byzantine Model Checker (ByMC). ByMC implements several techniques for automatic verification of threshold-guarded distributed algorithms. These algorithms have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and make 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. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that
involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.
URI: http://hdl.handle.net/20.500.12708/16502
DOI: 10.34726/422
Organisation: E192 - Institut für Logic and Computation 
License: Urheberrechtsschutz 1.0
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat Existing users please Login
main.pdf390.92 kBAdobe PDFEmbargoed until June 9, 2021    Request a copy
Show full item record

Page view(s)

checked on Feb 21, 2021


checked on Feb 21, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.