CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm

Hans Svensson (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Göteborg : Chalmers University of Technology, 2008. - 22 s.
[Rapport]

In 1997, Stoller presented a leader election algorithm for a synchronous system with crash failures. The algorithm is an adaptation of Garcia-Molina's Bully Algorithm that uses failure detectors instead of explicit timeouts. Since the characteristics of the algorithm closely resemble the Bully Algorithm Stoller does not give a formal correctness proof. However, although the algorithms appear similar, there are non-trivial differences. The differences make it unclear if the original proof, by Garcia-Molina, actually carries over as indicated by Stoller. In this document we formalize the leader election algorithm using first-order logic, and prove its correctness with respect to the obvious safety property; it should not be possible to elect two different leaders at the same time.



Denna post skapades 2008-03-17. Senast ändrad 2013-08-14.
CPL Pubid: 69237