Formal verification of ring-based leader election protocol using predicated diagrams

Abstract

Leader election is one of fundamental tasks in distributed computing. The objective of the protocol is for the processes among themselves to establish a designated process, called the leader. There are two basic properties that the leader election implementation needs to obey: (1) safety: it is never the case that there are two or more leaders at the same time and (2) liveness: in a stable situation (i.e. processes stop dying for a while), a leader will eventually be elected. In this researc.h we considered a ring-based leader election protocoi proposed by Chang and Roberts. We have proven or verified that this protocol satisfies the both properties. The proof is done by viewing the distributed systems as parameterized systems and using a class diagram called predicate diagrams* to do the verification. We use TLA* for formalization and use TLA+ style for writing specifications.