Leader Election

by Kim G. Larsen

We consider leader election in a ring topology. We assume that each node of the ring has a unique identifier. The object of the algorithm is to have all nodes identifying the (node with the) maximum identifier (above this is node 2 which has identifier 5). We consider the LCR algorithm (Lann, Chang and Roberts), where each process sends its identifier around the ring. When a process receives an incoming identifier, it compares that identifier to its own, it keeps passing the identifier; if it is less than its own, it discards the incoming identifier; if it is equal to its own, the process declares itself the leader.

We model as a timed automaton in UPPAAL the behavior of a node as illustrated to the left. The model and an associated query may be found here (simpleleader3.xml, simpleleader3.q).

Q1. Simulate the model and explain to what extent the model correspond to the informally given explanation above. You may want to (but you do not have to) modify the model.

Q2. Will a leader eventually be elected? What is the maximum amount of time before the leader is elected?

Q3. What is the maximum number of identifiers sent in the network before the leader is elected?

Q4. What is the expected time before a leader is elected?

Q5. What is the expected number of identifiers sent before the leader is elected?

Q6. Modify the model so that identifiers are only sent (before MaxD time-units) with a certain probability (say 70%). Investigate the effect of this on the properties (e.g. those above) of the protocol.

Q7- Investigate what happens if a node completely fails (e.g. by the transmission probability being 0%).

UPPAAL

You should download the UPPAAL 4.1.4 from www.uppaal.org.

Slides

Here.

Reading

· Various: Quasimodo Industrial Handbook on Quantitative Modeling and Analysis for Embedded Systems (draft, to be published by Springer)

· Aceto, Ingolfsdottir, Larsen, Srba: Reactive Systems: Modelling, Specification and Verification.  Cambridge University Press (Part II: A theory of real time systems).

· Uppaal pamphlet brief introduction to UPPAAL  on two pages.

· Behrmann, David, Larsen: A Tutorial on Uppaal

· Johan Bengtsson and Wang Yi: Timed Automata: Semantics, Algorithms and Tools. Concurrency and Petri Nets 2004, LNCS 3098.

· Ulrich Fahrenberg, Kim G. Larsen, Claus Thrane:   Verification, Performance Analysis and Controller Synthesis for Real-Time Systems. Marktoberdorf 2008 Lecture Notes. NATO ASI series, IOS Press Publishers, 2009.

Exercises (additional)

Here.