Refinement checking parameterised quorum systems

Abstract Many fault-tolerant algorithms are based on decisions made by a quorum of nodes. Since the algorithms are utilised in safety critical applications such as distributed databases, it is necessary to make sure that they operate reliably under every possible scenario. We introduce a generic compositional formalism, based on parameterised labelled transition systems, which allows us to express safety properties of parameterised quorum systems. We prove that any parameterised verification task expressible in the formalism collapses into finitely many finite state refinement checking problems. The technique is implemented in a tool, which performs the verification completely automatically. As an example, we prove the leader election phase of the Raft consensus algorithm correct for an arbitrary number of terms and for a cluster of any size