论文标题
使用阈值自动机和拜占庭模型检查器进行参数化验证的调查
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
论文作者
论文摘要
阈值守卫是许多耐故障算法的基本原始性，这些算法解决了分布式计算中的经典问题，例如可靠的广播，两相提交和共识。此外，在最近的区块链算法中可以找到阈值守卫，例如Tendermint共识。在本文中，我们概述了在拜占庭模型检查器（BYMC）中实现的阈值识别阈值耐耐故障分布式算法的技术。这些阈值保护算法具有以下功能：（1）最多$ t $的流程可能会崩溃或表现拜占庭； （2）正确的过程计算消息并在收到足够多消息时取得进展，例如至少$ t+1 $; （3）系统中流程的数字$ n $是一个参数，也是故障的数字$ t $； （4）参数受到弹性条件的限制，例如$ n> 3t $。传统上，这些算法是在具有多达十个参与过程的分布式系统中实施的。如今，它们已在涉及数百或数千个流程的分布式系统中实施。为了确保这些算法对于该比例仍然是正确的，必须为参数的所有可能值验证它们。
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as, e.g., Tendermint consensus. In this article, we give an overview of techniques for automated verification of threshold-guarded fault-tolerant distributed algorithms, implemented in the Byzantine Model Checker (ByMC). These threshold-guarded 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 the number $t$ of faults; and (4) 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.
