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

doi:10.1007/978-3-319-06200-6_3

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 proceeding › Chapter › peer-review

12 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 language	English
Title of host publication	NASA Formal Methods
Editors	Julia M. Badger, Kristin Yvonne Rozier
Publisher	Springer Verlag
Pages	31-45
Number of pages	16
Volume	8430 LNCS
ISBN (Print)	978-3-319-06199-3
DOIs	https://doi.org/10.1007/978-3-319-06200-6_3
Publication status	Published - 2014
Event	NASA Formal Methods: 6th International Symposium - NASA Johnson Space Center, Houston TX, United States Duration: 29 Apr 2014 → 1 May 2014 Conference number: 6th http://nasaformalmethods.org/2014/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8430

Conference

Conference	NASA Formal Methods
Abbreviated title	NFM 2014
Country/Territory	United States
City	Houston TX
Period	29/04/14 → 1/05/14
Internet address	http://nasaformalmethods.org/2014/

Keywords

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

Access to Document

10.1007/978-3-319-06200-6_3

Jeremy Bryans
- Centre for Future Transport and Cities - Assistant Professor Research
Person: Teaching and Research

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

Leadership election: An Industrial SoS application of compositional deadlock verification. / Antonino, Pedro R.G.; Oliveira, Marcel Medeiros; Sampaio, Augusto C.A. et al.
NASA Formal Methods. ed. / Julia M. Badger; Kristin Yvonne Rozier. Vol. 8430 LNCS Springer Verlag, 2014. p. 31-45 (Lecture Notes in Computer Science; Vol. 8430).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Antonino, PRG, Oliveira, MM, Sampaio, ACA, Kristensen, KE & Bryans, JW 2014, Leadership election: An Industrial SoS application of compositional deadlock verification. in JM Badger & KY Rozier (eds), NASA Formal Methods. vol. 8430 LNCS, Lecture Notes in Computer Science, vol. 8430, Springer Verlag, pp. 31-45, NASA Formal Methods, Houston TX, United States, 29/04/14. https://doi.org/10.1007/978-3-319-06200-6_3

@inbook{72759009fb6d4351b9bcf6b2cccc2165,

title = "Leadership election: An Industrial SoS application of compositional deadlock verification",

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.",

keywords = "Software Engineering, Programming Languages, Compilers, Interpreters, Operating Systems, Logics and Meanings of Programs, Software Engineering/Programming and Operating Systems, Programming Techniques",

author = "Antonino, {Pedro R.G.} and Oliveira, {Marcel Medeiros} and Sampaio, {Augusto C.A.} and Kristensen, {Klaus E.} and J.W. Bryans",

year = "2014",

doi = "10.1007/978-3-319-06200-6_3",

language = "English",

isbn = "978-3-319-06199-3",

volume = "8430 LNCS",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "31--45",

editor = "Badger, {Julia M.} and Rozier, {Kristin Yvonne}",

booktitle = "NASA Formal Methods",

address = "Austria",

note = "NASA Formal Methods : 6th International Symposium, NFM 2014 ; Conference date: 29-04-2014 Through 01-05-2014",

url = "http://nasaformalmethods.org/2014/",

}

TY - CHAP

T1 - Leadership election

T2 - NASA Formal Methods

AU - Antonino, Pedro R.G.

AU - Oliveira, Marcel Medeiros

AU - Sampaio, Augusto C.A.

AU - Kristensen, Klaus E.

AU - Bryans, J.W.

N1 - Conference code: 6th

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Software Engineering

KW - Programming Languages

KW - Compilers

KW - Interpreters

KW - Operating Systems

KW - Logics and Meanings of Programs

KW - Software Engineering/Programming and Operating Systems

KW - Programming Techniques

U2 - 10.1007/978-3-319-06200-6_3

DO - 10.1007/978-3-319-06200-6_3

M3 - Chapter

SN - 978-3-319-06199-3

VL - 8430 LNCS

T3 - Lecture Notes in Computer Science

SP - 31

EP - 45

BT - NASA Formal Methods

A2 - Badger, Julia M.

A2 - Rozier, Kristin Yvonne

PB - Springer Verlag

Y2 - 29 April 2014 through 1 May 2014

ER -

Leadership election: An Industrial SoS application of compositional deadlock verification

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Profiles

Jeremy Bryans

Cite this