Tutorial: Parameterized Verification with Byzantine Model Checker
| Autor: | Ilina Stoilkovska, Josef Widder, Igor Konnov, Marijana Lazić |
|---|---|
| Přispěvatelé: | Informal systems [Vienna], Technische Universität Munchen - Université Technique de Munich [Munich, Allemagne] (TUM), Vienna University of Technology (TU Wien), Alexey Gotsman, Ana Sokolova, TC 6, WG 6.1, Technical University of Munich (TUM) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Model checking
Theoretical computer science Computer science Parameterized complexity Scale (descriptive set theory) 0102 computer and information sciences 02 engineering and technology Commit 01 natural sciences Article [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] 010201 computation theory & mathematics Distributed algorithm 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] Resilience (network) |
| Zdroj: | Formal Techniques for Distributed Objects, Components, and Systems Lecture Notes in Computer Science 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE) 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.189-207, ⟨10.1007/978-3-030-50086-3_11⟩ Lecture Notes in Computer Science-Formal Techniques for Distributed Objects, Components, and Systems Formal Techniques for Distributed Objects, Components, and Systems-FORTE 2020 Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783030500856 FORTE |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-50086-3_11⟩ |
| Popis: | 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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$t+1$$\end{document}; (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., \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$n > 3t$$\end{document}. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|