DocumentCode :
1897556
Title :
Model Checking of Consensus Algorit
Author :
Tsuchiya, Tatsuhiro ; Schiper, André
Author_Institution :
Osaka Univ., Suita
fYear :
2007
fDate :
10-12 Oct. 2007
Firstpage :
137
Lastpage :
148
Abstract :
We show for the first time that standard model checking allows one to completely verify asynchronous algorithms for solving consensus, a fundamental problem in fault-tolerant distributed computing. Model checking is a powerful verification methodology based on state exploration. However it has rarely been applied to consensus algorithms, because these algorithms induce huge, often infinite state spaces. Here we focus on consensus algorithms based on the Heard-Of model, a new computation model for distributed computing. By making use of the high abstraction level provided by this computation model and by devising a finite representation of unbounded timestamps, we develop a methodology for verifying consensus algorithms in every possible state by model checking.
Keywords :
distributed algorithms; formal verification; asynchronous algorithm verification; consensus algorithm model checking; fault-tolerant distributed computing; finite unbounded timestamp representation; heard-of model; Algorithm design and analysis; Computational modeling; Distributed algorithms; Distributed computing; Fault tolerance; Fault tolerant systems; Formal verification; Mathematical model; Power system modeling; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Reliable Distributed Systems, 2007. SRDS 2007. 26th IEEE International Symposium on
Conference_Location :
Beijing
ISSN :
1060-9857
Print_ISBN :
0-7695-2995-X
Type :
conf
DOI :
10.1109/SRDS.2007.20
Filename :
4365691
Link To Document :
بازگشت