Test and Verification

Modelling Exercises

Exercises

Choose one of the five exercises below. Your solution should contain two part, a main part containing modeling and analyses of the particular system you have chosen using either UPPAAL or visualSTATE (or both). Also the solution should contain a secondary part providing an evaluation of the tool used. You may hand in solutions in groups with at most 3 persons. The solution should be some 5-7 typeset pages. We will assisting you on March 10 (Thursday) and March 17 (Thursday after the lecture) in the PC-Lab. The complete report should be delivered on April 15 (Friday) at noon.

Exercise 1 (Washing Machine)

Model and analyze the control program of a washing machine:

A program selector controls the machine. Functionality is as follows,

• Water is taken in through 1 of 3 valves. Water for pre-washing is taken in through Valve 1, water for rinsing is taken in through Valve 2 and water for main-wash is taken in through Valve 3.
• When starting the pump, used water is pumped out. A sensor tells when the machine is empty of water, or when the machine is full of water.
• An engine turns the washing cylinder in both right and left direction. The engine runs slowly during washing and fast during spinning. When spinning the direction is not changed.
• During washing the cylinder turns 6 times to the right and 6 times to the left. A pulse counter register each time the cylinder passes the top point.

The control is as follows:

• There is only one washing program.
• The pre-wash runs for 7 minutes.
• Rinsing runs for 3 minutes.
• The main wash runs for 9 minutes.
• Rinsing runs for 3 minutes.
• The pump runs until the machine is empty of water.
• There is only one rinse after the main wash and one rinse after pre-wash.
• Spinning speed is twice the normal wash speed and is running for 1 minute

Exercise 2 (Elevator system)

Model and analyze a control system of an elevator, with the following functionality:

• The elevator is controlled by only one button by which it is possible to order the elevator to the floor where you stand.
• The elevator comprises three floors meaning that the elevator cannot move directly from floor 1 to 3, but must pass through floor 2. Consequently movement from floor 3 to 1 requires passing floor 2.
• The elevator's initial position is floor 1.
• Pressing a button on a certain floor means that the elevator moves to that floor.
• For security reasons, it should only be possible to open the door when the selected floor is reached.

Possibly also model the elevator itself including assumption of the time to get from one floor to another. Try to validate various safety and progress properties that you may want the system to satisfy.

Exercise 3 (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).

Exercise 4 (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.

Exercise 5 (Crossing the River)

• Max 2 persons on the boat,
• Mom not alone with boys,
• Dad ont alone with girls,
• Thief not alone with family,
• Only police officer, dad and mom can handle the boat.

Task 1: Make an Uppaal model of it and generate a feasible schedule.

Task 2: Add temporal constraints (e.g. each adult take a certain time to cross the river with the boat) and try to find the quickest possible schedule.

Task 3: Try other parameters and constraints for this game. Determine what is the feasibility limit depending on the number of boys, girls, prisonners.