Test and Verification 2007

Modelling Exercises

Requirements to your solution

Choose one of the five exercises below. Your solution should contain two parts, a main part containing in a documented fashion the modeling and analyses of the particular system you have chosen using UPPAAL 4.0 (see www.uppaal.com).  Also your solution should ideally contain a shorter secondary part possibly addressing

You may hand in solutions in groups with at most 3 persons. The solution should be some 5-10 typeset pages. The complete report should be delivered on

Exercise 1 (Elevator system)

Model and analyze a control system of an elevator-system of your own design serving a number of floors (say 4 or 5) and with a number of lifts (say 2 or 3) and with a number of users being on individual floors and with individual wishes for getting to different floors. The system may:

In modelling the elevator system itself assumption of the time to get from one floor to another. Also model timing assumptions as to the arrivial of users of the elevator system.  Try to validate various safety and progress properties that you may want the system to satisfy.

Exercise 2 (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:

Notice that you should not model topology changes (network links appearing or disappearing).

A few tips for your modeling work:

Exercise 4 (Rush Hour)

In this exercise you are asked to model a solitaire game and use UPPAAL to solve the puzzle. The game is simple. You have a 6x6 board as shown on the picture below. On the board you find a number of cars of different sizes (personal vehicles and trucks). The goal of the game is to move the cars and trucks 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!


Special challenge: you may want to deal with the more challenging RAILROAD Rush Hour, which is on a 7x7 boards and with 2x2 blockers that can move bort horizontal and vertical (see figure below).  Again the objective is to get the RED train out of the exit (to the right).

 

Exercise 5 (Crossing the River)

Help a familly shown below to cross a river according to the following constraints (click on the picture or here to activate an interactive version of this puzzle):