Assignment: Analysis of a Leader Election Protocol in Uppaal

Solve the following problem in Uppaal. You should:

1. model this protocol as a network of timed automata in Uppaal,
2. assess the quality of the model using the criteria described in section 1.10 of the paper A First Introduction to Uppaal
3. use your model to answer the verification questions given in the text below,
4. write a report about your model, documenting how it works, why you chose to model the problem like you did, and how you can answer the verification questions.

The Protocol

In this assignment we consider a simple leader election protocol. The setting is the following. There are a number of interconnected network nodes. Each node has an address. The goal of the protocol is to identify the node with the lowest address is the network and elect that node to be the leader. In order to be correct, all connected nodes should elect the same leader.

As part of the protocol, each node maintains information about which node it thinks is the leader and the number of hops (network links) to the leader. Let's say that the information at node i is stored as a pair ni=(l, h). It is perfectly valid for a node to believe that itself is the leader and in this case the number of hops to the leader is 0, e.g. n1=(1,0).

Within th protocol nodes transmit messages of the form m=(source, destination, leader, hops) to each other. Here source is the address of the node sending the message, destination is the address of the node receiving the message, leader is information about which node source thinks is the leader and hops is the number of hops (network links) between the source and the leader.

Whenever a node i receives a message m, it compares the m.leader and m.hops fields in the message with the local information ni it already has. If the leader address in the message is bigger than the address of the previous leader known to the node, i.e. m.leader > ni.leader, then the message is discarded. If the leader is the same, but the number of hops is bigger than the previous number of hops known, i.e. m.leader = ni.leader and m.hops > ni.hops, then the message is discarded. Otherwise the internal information stored at the node, i.e. ni is set to (m.leader, m.hops).

Whenever ni is updated, node i sends a message m=(i, d, ni.leader, ni.hops) to each of its neighbours d, with the exception that it does not send a message back to the source of message which triggered the update in the first place. There is an upper time bound on the arrival of the message called MSG_DELAY. Notice that there is no lower bound on the delivery time and that messages might be reordered.

The final ingredient of the protocol is a timeout mechanism. If a node has not receive any messages, except those which are discarded, for more than a certain timeout period, then a timeout will happen within TIMEOUT_DELAY time units (i.e. there is a reaction delay) -- this means that there is actually a range of ]timeout; timeout+TIMEOUT_DELAY] after the last receiption of a "good" message in which a timeout will happen. Initially, the timeout is a constant INITIAL_TIMEOUT. When receiving good messages (messages which do not contain worse information than what we already got), then the timeout is set to INITIAL_TIMEOUT + TIMEOUT_DELAY + ni.hops * MESSAGE_DELAY. When a node times out, it will elect itself as the new leader and send an update message to all its neighbors.

Questions

Your task is to:

• model an instance of the above protocol with three connected nodes (e.g. a fully connected topology - this might be the simplest to model) and the following constants:

  Constant	Value
  INITIAL_TIMEOUT	10
  TIMEOUT_DELAY	5
  MESSAGE_DELAY	3

• use the simulator to convince yourself that it works as intended
• verify that your model is deadlock free
• verify that it is possible for the system to come in a state, where all nodes know the correct leader
• verify that it is always the case that a node i knows the correct leader after TIMEOUT + TIMEOUT_DELAY + DISTANCEi * MSG_DELAY, where DISTANCEi is the real number of hops from i to the correct leader.
• consider a few alternative network topologies; what is the maximal network size Uppaal can handle?
• Bonus: How about a general verification for all topologies and parameter values?

Notice that you do no need to model dynamic topology changes (network links appearing or disappearing).

A few tips for your modeling work:

• Make a node template for modeling a node. Instantiate it once for each node of the network.
• Make a message template, which is used to represent a message. You will need a number of instances of this template. For 3 nodes, 10 should suffice. Use the model checker to verify that you do indeed have enough message processes.
• You can use shared variables and channels for the communication between the node processes and the message processes.
• Initially, before any messages are sent, each node believes it is the leader (like in the first figure).