2014/08/26 by Giorgio Delzanno, Michele Tatarek, Riccardo Traverso
Computer Science · #cs.LO #cs.DC #cs.DM
paper · pdf · doi:10.4204/eptcs.161.13
published as EPTCS 161, 2014, pp. 131-146 · In Proceedings GandALF 2014, arXiv:1408.5560
arxiv created 2014/08/26 · arxiv updated 2014/08/27
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.