Safety Verification of Asynchronous Consensus Algorithms with Model Checking

This paper proposes a model checking-based approach to verification of asynchronous consensus algorithms, an important class of distributed fault-tolerant algorithms. The proposed approach can be used to verify these algorithms against agreement, which is the key safety property of this class of algorithms. A consensus algorithm typically has runs of unbounded length and unbounded queues or sets of messages in transit, thus its state space is often infinite. This property makes application of model checking difficult, because model checking is based on state space exploration. Our approach can limit the use of model checking to a single round of an algorithm, by using a finite state model that over approximates the behavior of any single round. As a result, the problem of infinite state spaces can be circumvented. In case studies, two consensus algorithms are verified using this approach.