Giorgio Delzanno (DIBRIS, University of Genova) |
Michele Tatarek (DIBRIS, University of Genova) |
Riccardo Traverso (FBK, Trento) |
We present a formal model of a distributed consensus algorithm in the executable specification language Promela extended with a new type of guards, called counting guards, needed to implement transitions that depend on majority voting. Our formalization exploits abstractions that follow from reduction theorems applied to the specific case-study. We apply the model checker Spin to automatically validate finite instances of the model and to extract preconditions on the size of quorums used in the election phases of the protocol. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.161.13 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |