171619
20190316235240.0
doi
10.1007/s00446-010-0123-3
0178-2770
ISI
000288716600004
ARTICLE
Verification of consensus algorithms using satisfiability solving
2011
Springer Verlag
2011
Journal Articles
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.
Consensus
Model checking
Fault-tolerant distributed algorithms
Formal verification
Bounded Model Checking
Distributed Consensus
Automated Verification
Agreement
Induction
Systems
Solver
Paxos
Time
Tsuchiya, Tatsuhiro
241767
Schiper, Andre
106377
23
341-358
Distributed Computing
994530
http://infoscience.epfl.ch/record/171619/files/MC.pdf
n/a
n/a
252206
LSR
U10411
oai:infoscience.tind.io:171619
IC
article
GLOBAL_SET
106377
EPFL-ARTICLE-171619
EPFL
REVIEWED
PUBLISHED
ARTICLE