Test and Verification

Lecture 14-15

Subject

        Modelling Exercise

Exercises

Choose one of the three 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 April 2 (Wednesday) and April 14 (Monday) in the PC-Lab.  NOTE the change of dates (due to conference participation and Easter coming up).

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 (Gossiping Girls)

Model and analyze the following gossiping girls problem. A number of girls initially know one distinct secret each. Each girl have access to a phone which can be used to call another girl to share their secrets. Each time two girls talk to each other they always exchange all secrets with each other (thus after the phone call they both know all secrets they knew together before the phone call). Only binary commmunication (between two girls in each phone call) is possible.

Task 1: Find the minimal number of phone calls needed for four girls to know all secrets.

Task 2: Try to find an (inductive) argument for how many phone calls are needed to solve the gossiping girls problem for n girls.

Task 3: Refine your model so that each phone call requires some start time units to connect, and in addition some transfer time units to exchange each secret. Find the minimum time needed to solve the gossiping girls problem for four girls if start is 30 and transfer is 60.  Try to vary the number of telephone lines (one, two, arbitrarily many).

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