Verification of consensus algorithms using satisfiability solving

作     者：Tsuchiya, Tatsuhiro Schiper, Andre 

作者机构：Osaka Univ Suita Osaka 5650871 Japan Ecole Polytech Fed Lausanne CH-1015 Lausanne Switzerland 

出 版 物：《DISTRIBUTED COMPUTING》 (分布式计算)

年 卷 期：2011年第23卷第5-6期

页      面：341-358页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Japanese Ministry of Education, Science, Sports and Culture Swiss National Science Foundation [200021-111701] Hasler Foundation Grants-in-Aid for Scientific Research Funding Source: KAKEN 

主　　题：Consensus Model checking Fault-tolerant distributed algorithms Formal verification 

摘      要：Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. 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 small, 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 several consensus algorithms up to around 10 processes.