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 proceedingChapter

    10 Citations (Scopus)

    Abstract

    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
    Pages31-45
    Number of pages16
    Volume8430 LNCS
    ISBN (Print)978-3-319-06199-3
    DOIs
    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
    http://nasaformalmethods.org/2014/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume8430

    Conference

    ConferenceNASA Formal Methods
    Abbreviated titleNFM 2014
    CountryUnited States
    CityHouston TX
    Period29/04/141/05/14
    Internet address

    Keywords

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

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

  • Cite this

    Antonino, P. R. G., Oliveira, M. M., Sampaio, A. C. A., Kristensen, K. E., & Bryans, J. W. (2014). Leadership election: An Industrial SoS application of compositional deadlock verification. In J. M. Badger, & K. Y. Rozier (Eds.), NASA Formal Methods (Vol. 8430 LNCS, pp. 31-45). (Lecture Notes in Computer Science; Vol. 8430). Springer Verlag. https://doi.org/10.1007/978-3-319-06200-6_3