Towards Automated Verification of Distributed Consensus Protocols

This paper presents an approach to facilitating model checking of consensus protocols, a class of distributed protocols. Model checking is a successful formal verification method. However its application to these protocols is still not a common practice because of the following problems. First, model checking requires non-negligible users´ efforts in representing the protocol under verification in the input language of a model checker. Second, these protocols usually induce an infinite state space, making model checking infeasible. To alleviate these problems, the proposed approach provides (i) a language for concisely describing consensus protocols and (ii) a translator from the proposed language to a mathematical formula that symbolically represents the entire behavior of the protocol. Once the formula is generated, one can model check the protocol by checking the satisfiability of the formula with a satisfiability modulo theories (SMT) solver. Several case studies demonstrate the usefulness of the proposed approach both in correctness proving and bug hunting.