Formal verification of a leader election protocol in process algebra

L.A.A. Fredlund, J.F. Groote, H. Korver

Research output: Contribution to journalArticleAcademicpeer-review

15 Citations (Scopus)

Abstract

In 1982 Dolev, et al. [10] presented an O(nlogn) 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.
Original languageEnglish
Pages (from-to)459-486
Number of pages28
JournalTheoretical Computer Science
Volume177
Issue number2
DOIs
Publication statusPublished - 1997

Fingerprint

Dive into the research topics of 'Formal verification of a leader election protocol in process algebra'. Together they form a unique fingerprint.

Cite this