A Proof of a Leader Election Protocol in microCRL ($\mu$CRL)

Fredlund, Lars-Åke and Groote, Jan Friso and Korver, Henri (1995) A Proof of a Leader Election Protocol in microCRL ($\mu$CRL). [SICS Report]



In 1982 Dolev, Klawe & Rodeh presented an O(n log n) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem}. At the same time Peterson came up with a nearly identical solution. In this paper, we bring the correctness of this algorithm to a completely formal level. This relatively small protocol, which can be described on half a page, requires a rather involved proof for guaranteeing that it behaves well in all possible circumstances. To our knowledge, this is one of the more advanced case-studies in formal verification based on process algebra.

Item Type:SICS Report
Uncontrolled Keywords:Formal Methods, Process algebra, Protocol verification
ID Code:2142
Deposited By:Vicki Carleson
Deposited On:26 Oct 2007
Last Modified:18 Nov 2009 16:00

Repository Staff Only: item control page