Analysis of a leader election algorithm in μCRL

This paper investigates the applicability of formal methods for the specification and verification of distributed algorithms. The problem of election is an important class of distributed algorithms that are widely studied in the literatures. We prove the correctness of a representative leader election algorithm, that is, the LCR algorithm, developed by LeLann, Chang and Roberts. This algorithm is one of the early election algorithms and serves as a nice benchmark for verification exercises. The verification is based on the μCRL, which is a language for specifying distributed systems and algorithms in an algebraic style and combines the process algebra and (equational) data types. We bring the correctness of the algorithm to a completely formal level. It turns out that this relatively "small" and "simple" algorithm requires a rather involved proof for guaranteeing that it behaves well in all possible circumstance. This paper demonstrates the possibility to deliver completely formal and mechanically verifiable correctness proofs of highly nondeterministic distributed algorithm, which is indispensable in the design and implementation of distributed algorithm and systems.