Formal verification of a leader election protocol in process algebra

In 1982 Dolev, et al. [10] presented an O( nlog 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...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 1997-05, Vol.177 (2), p.459-486
Main Authors: Fredlund, Lars-åke, Groote, Jan Friso, Korver, Henri
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In 1982 Dolev, et al. [10] presented an O( nlog 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.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(96)00256-3