Using Bounded Model Checking to Verify Consensus Algorithms
Using Bounded Model Checking to Verify Consensus Algorithms
复制标题
DOI：
10.1007/978-3-540-87779-0_32
复制
发表时间：
2008-09
期刊：
影响因子：
--
通讯作者：
Tatsuhiro Tsuchiya;A. Schiper
中科院分区：
文献类型：
--
作者：
Tatsuhiro Tsuchiya;A. Schiper
提出了一种异步轮一致性算法的自动验证方法。我们使用模型检查，广泛实践的验证方法，但它的应用程序异步分布式算法是困难的，因为这些算法的状态空间往往是无限的。所提出的方法解决了这一困难，通过减少验证问题的小模型检查问题，只涉及单一阶段的算法执行。由于一个阶段由有限个轮组成，有界模型检测，一种使用可满足性求解的技术，可以有效地用于解决这些问题。所提出的方法允许我们模型检查一些共识算法多达10个左右的进程。
This paper presents an approach to automatic verification of asynchronous round-based consensus algorithms. We use model checking, a widely practiced verification method; but its application to asynchronous distributed algorithms is difficult because the state space of these algorithms is often infinite. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check some consensus algorithms up to around 10 processes.