Sciweavers

ICECCS
2010
IEEE

Model Checking Round-Based Distributed Algorithms

13 years 10 months ago
Model Checking Round-Based Distributed Algorithms
—In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking. In this paper, we present a general idea of investigating the bounded distance of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make automatic verification of these algorithms possible. We apply this idea to several algorithms and present their verification results in the model checker Spin.
Xin An, Jun Pang
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where ICECCS
Authors Xin An, Jun Pang
Comments (0)