Sciweavers

Share
CAV
2001
Springer

Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM

11 years 12 months ago
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM
We consider the randomized consensus protocol of Aspnes and Herlihy for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The algorithm guarantees termination in the presence of stopping failures within polynomial expected time. Processes proceed through possibly unboundedly many rounds; at each round, they read the status of all other processes and attempt to agree. Each attempt involves a distributed random walk: when processes disagree, a shared coin-flipping protocol is used to decide their next preferred value. Achieving polynomial expected time depends on the probability that all processes draw the same value being above an appropriate bound. For the non-probabilistic part of the algorithm, we use the proof assistant Cadence SMV to prove validity and agreement for all N and for all rounds. The coin-flipping protocol is verified using the probabilistic model checker PRISM. For a finite number of processes (up to 10) we automatical...
Marta Z. Kwiatkowska, Gethin Norman, Roberto Segal
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where CAV
Authors Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala
Comments (0)
books