Formal analysis of consensus protocols in asynchronous distributed systems

This paper presents a formal veriffication of two consensus protocols for distributed systems presented in [T. Deepak Chandra and S. Toueg, Unreliable failure detectors for reliable distributed systems, J. ACM, 1996]. These two protocols rely on two underlying failure detection protocols. We formalize an abstract model of the underlying failure detection protocols and building upon this abstract model, formalize the two consensus protocols. We prove that both algorithms satisfy the properties of "uniform agreement","uniform integrity", "termination" and "uniform validity" assuming the correctness of their corresponding failure detectors.