Leadership election: An Industrial SoS application of compositional deadlock verification

Pedro R.G. Antonino, Marcel Medeiros Oliveira, Augusto C.A. Sampaio, Klaus E. Kristensen, J.W. Bryans

    Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

    11 Citations (Scopus)


    In distributed computing, the leadership election has been used to distributively designate a node as the central controller (leader) of a network of nodes. The complexity of the algorithm arises due to the unawareness of every node of who the current leader is. After running the algorithm, however, a unique node in the network must be elected as the leader and recognized as so by the remaining nodes. In this paper, using CSP, we formalise the leadership election algorithm used by our industrial partner. Its verification is feasible only due to the use of a pattern based strategy that allows the verification to be carried out in a fully local manner. The pattern used here is novel and a further contribution of the paper. A refinement relation together with predicate abstraction is used to describe pattern conformance. The mechanisation of the behavioural conformance is carried out using FDR.
    Original languageEnglish
    Title of host publicationNASA Formal Methods
    EditorsJulia M. Badger, Kristin Yvonne Rozier
    PublisherSpringer Verlag
    Number of pages16
    Volume8430 LNCS
    ISBN (Print)978-3-319-06199-3
    Publication statusPublished - 2014
    EventNASA Formal Methods: 6th International Symposium - NASA Johnson Space Center, Houston TX, United States
    Duration: 29 Apr 20141 May 2014
    Conference number: 6th

    Publication series

    NameLecture Notes in Computer Science


    ConferenceNASA Formal Methods
    Abbreviated titleNFM 2014
    Country/TerritoryUnited States
    CityHouston TX
    Internet address


    • Software Engineering
    • Programming Languages
    • Compilers
    • Interpreters
    • Operating Systems
    • Logics and Meanings of Programs
    • Software Engineering/Programming and Operating Systems
    • Programming Techniques


    Dive into the research topics of 'Leadership election: An Industrial SoS application of compositional deadlock verification'. Together they form a unique fingerprint.

    Cite this