Paper Info
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.
Year
DOI
Venue
2014
10.1007/978-3-319-06200-6_3
Lecture Notes in Computer Science
Keywords
Field
DocType
Leadership Election,Local Analysis,Deadlock Freedom
Programming language,Predicate abstraction,Computer science,Deadlock,Theoretical computer science,Compiler,Interpreter,Local analysis
Conference
Volume
ISSN
Citations 
8430
0302-9743
4
PageRank 
References 
Authors
0.44
10
5
Name
Order
Citations
PageRank
Pedro R. G. Antonino1334.57
Marcel Medeiros Oliveira240.44
Augusto Sampaio350143.38
Klaus E. Kristensen440.78
Jeremy W. Bryans517513.88