The Major Excercise

In order to pass the course, you need to solve one of the major exercises and hand in a small report documenting your work. You should choose one of the three modeling exercises presented below. Alternatively, if you as part of your research have a similar modeling problem, then you can approach us about using this problem as the major excercise for passing the course -- but consult us about this before your start.

All problems are to be solved in Uppaal. You can download new newest version from the Uppaal Homepage. Each exercise text is presenting a problem. You should:

1. model this problem as a network of timed automata in Uppaal,
2. use your model to answer some of the verification questions given in the exercise text,
3. write a small report (5 pages) 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.

You should hand in the report and the models to Gerd Behrmann, either by mail (PostScript or PDF files for the report are preferred) or in print.

The deadline for handing in the report is the 5th of December, 2003.

CSMA/CD Protocol

The Carrier Sense Multible Access with Collision Detection (CSMA/CD) protocol is used in commodity Ethernet NICs to avoid, detect and resolve collissions on the shared ethernet bus.

Your task is to model the Medium Access Control (MAC) sublayer of the protocol. You should consider a simple configuration with only two nodes: The protocol specification consists of two MAC entities, MAC1 and MAC2, interconnected by a bi-directional medium M. The MAC entities are identical and can both transmit and receive messages over the medium. This means that collisions may occur on the medium (if the two MAC's transmit simultaneously). It is assumed that collisions will be detected in the medium and signaled to both MAC1 and MAC2.

Overview of the MAC sub layer.

A model of the protocol is given in csma-cd-start.xml (the specification is taken from "Verifying a CSMA/CD Protocol with CCS" by Joachim Parrow. The specification uses the following synchronization actions to describe the protocol events:

• send - service provided by Mac which reacts by transmitting a message,
• rec - (receive) service provided by Mac, indicates that a message is ready to be received,
• b - (begin) Mac begins message transmission to M,
• e - (end) Mac terminates message transmission to M,
• br - (begin receive) M begins message delivery to Mac,
• er - (end receive) M terminates message delivery to Mac,
• c - (collision) Mac is notified that a collision has occurred on M.

Note that a message transmission is not modeled by a single action. Instead the start of a transmission and the end of a transmission are modeled by two separate actions (the actions b(r) and e(r)). This is needed as there may be collisions detected in the middle of a transmission. Note also that we use indexes on all actions as there are two identical MAC entities.

MAC1.

Initially, MAC1 accepts a service call (send1?). The MAC initiates transmission (b1!), unless a message is in the process of being received. If the transmission is successfully terminated (e1!) new messages can be transmitted and the process is repeated. If a collision occurs (c1?) the MAC attempts re-transmission of the message. In all states (except when a message is being transmitted) the MAC is willing to start receiving. A message may be received (br1?) after which the MAC may not begin message transmission before the end of message (er1?) has been received and the MAC has signaled that the message is ready to be delivered (rec1!). However, the MAC may receive a send request (send1?) if there is not already another request waiting.

The medium M.

Initially, the medium accepts transmission from one of the MAC's (b1? or b2?). We assume MAC1 (b1?) starts transmitting first (the case for b2? is symmetric). The medium is assumed to be "half-duplex" meaning that a full message must be transmitted (br2!, e1?, er2!) before the next message can be accepted. If the receiving MAC (i.e. MAC2) starts transmission (b2?) the medium interrupts the transmission and signals collision (c1!, c2!) to both MAC1 and MAC1 (in any order).

Task 1: Open the protocol specification in csma-cd-start.xml and add a test environment that "uses" the protocol. Validate that your system is functionally correct using UPPAAL's simulator.

Task 2: Check (by verification) if the system is correct in the sense that sent messages are received. How many messages can be in transfer at the same time? Is it 1, 2 or more messages?

The model of the MAC is slightly inaccurate. In reality, a MAC would be two processes: one sender performing the actions send!, b!, e!, c? and one receiver performing the actions rec!, br? and er?

Task 3: Refine the protocol by letting each MAC consist of two processes, a sender (S) and a receiver (R). The idea is to let S perform all "horizontal" transitions and R all "vertical" transitions. Replace MAC with S and R. Use UPPAAL to validate and verify that the protocol no longer is correct.

Task 4: Redefine the protocol again so that it works, while still keeping the S and R separate. This is a bit tricky. You may need to add some synchronization channels (or data variables) to achieve synchronization between S and R.

You are now asked to refine the model so that the sent messages have a fixed length of time length, and to refine the communication medium M to have a communication delay of time delay..

Task 5: Model/modify the system with the assumption length<delay.

Task 6: Verify that the system is correct in the sense that all sent messages are indeed received..

Task 7: Refine the medium to allow messages of length length>=delay.

Task 8: Verify that the refined system is correct in the sense that all sent messages are indeed received.

Leader Election Protocol

In this exercise you will 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 have elected 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).

The protocol transmits messages on the form m=(source, destination, leader, hops) between the nodes. 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 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.

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

Notice that you should not model 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).

Rush Hour

In this exercise you are asked to model a solitair game and solve use UPPAAL to solve the puzzle. The game is simple. You have a 6x6 board like shown on the picture below. On the board you find a number of cars of different size (personal vehicles and trucks). The goal of the game is to move the cars by driving forward and backwards in such a way that the red car can leave the board at the exit on the right side of the board. The cars cannot turn!

Task 1: Make a model of the game in UPPAAL.

Task 2: Use your model to solve the two puzzles shown in he second picture. What is the shortest number of steps/moves needed to solve the puzzle?

Task 3: Extend your model with timing constraint. Assume that it takes a different amount of time to move the cars, e.g. 2 time units for the small ones and 3 for the trucks (you can also choose to give each car its own time). Try to experiment with different assumptions as to the number of hands/drivers, i.e. how many cars can move at the same time.