Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks

Jacob Brunekreef, Joost-Pieter Katoen, Ron Koymans, Sjouke Mauw

    Research output: Contribution to journalArticleAcademicpeer-review

    47 Citations (Scopus)
    30 Downloads (Pure)

    Abstract

    The well-known problem of leader election in distributed systems is considered in a dynamic context where processes may participate and crash spontaneously. Processes communicate by means of buffered broadcasting as opposed to usual point-to-point communication. In this paper we design a leader election protocol in such a dynamic context. As the problem at hand is considerably complex we develop the protocol in three steps. In the initial design processes are considered to be perfect and a leader is assumed to be present initially. In the second protocol, the assumption of an initial leader is dropped. This leads to a symmetric protocol which uses an () timeout mechanism to detect the absence of a leader. Finally, in the last step of the design processes may crash without giving any notification of other processes. The worst case message complexity of all protocols is addressed. A formal approach to the specification and verification of the leader election protocols is adopted. The requirements are specified in a property-oriented way and the protocols are denoted by means of extended finite state machines. It is proven using linear-time temporal logic that the fault-tolerant protocol satisfies its requirements.
    Original languageEnglish
    Pages (from-to)157-171
    Number of pages15
    JournalDistributed computing
    Volume9
    Issue number4
    DOIs
    Publication statusPublished - Feb 1996

    Keywords

    • FMT-CBD: CORRECTNESS BY DESIGN
    • Broadcast network
    • Communication protocols
    • Finite-state machines
    • Leader election
    • Message complexity
    • Protocol design, specification, and verification
    • Temporal logic

    Fingerprint Dive into the research topics of 'Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks'. Together they form a unique fingerprint.

    Cite this