Modelling in UPPAAL

The assignment should give the student a chance to use a tool for modeling and formal analysis of real-time systems.

The assignment should be solved individually or in groups of two. The assignment must be handed in no later than 2002-12-19.

UPPAAL

On the Unix machines at DoCS UPPAAL is started using the script uppaal2k.sh. Copy the script to a location in your execution PATH and make it executable with `chmod u+x uppaal2k.sh'.

In section Working@Home below you may find instruction on how to download and run Uppaal at home.

If you get problems running UPPAAL take a careful look at the error messages and report them to the teaching assistant. Especially if it complains about "Could not connect to server", click "No" in the pop-up window and go to the Verifier tab. The section at the bottom contain the error message.

Useful documentation on UPPAAL is the UPPAAL2k: Small Tutorial and UPPAAL in a Nutshell. Also investigate the help menu in the UPPAAL tool.

A Coffee Machine

The main purpose of this assignment is to make you more comfortable with the UPPAAL tool. To that end you may also read the tutorial.

As you all know, large amount of coffee is a necessity to produce good results, (especially in academia). This first assignment lets you construct a system which maximises the number of (academic) publications produced.

You are asked to design the control of a (coffee) Machine (the control program) which will serve a coffee craving Person (eg. a PhD student). As you can see above the Person repeatedly (tries to) insert a coin, (tries to) extract coffee after which (s)he will make a publication. Between each action the Person requires a suitable time-delay before being ready to participate in the next one.

After receiving a coin the Machine should take some time for brewing the coffee. The Machine should time-out if the brewed coffee has not been taken before a certain upper time-limit.

As a requirement we want the overall behaviour to ensure that the indicated Observer (eg. some demanding professor or funding institute) experiences a constant flow of publications from the Person. In particular we want the Observer to complain if at any time more than 8 time-units elapses between two consecutive publications. Model the Machine and Observer in UPPAAL and analyse the behaviour of the system. You must use the Verifier to determine this.

After creating the Machine, Person and Observer automata, try to determine the maximum brewing time allowed by the Machine in order that the above requirements is met. Also here the Verifier will help you.

Modelling Tips:

• You can use the Verifier and E<> - (is there a state in the system where the statement is true?) and A[] - (is the statement true in all states of the system?) specifications to give questions to the system and generate traces (turn on the diagnostic trace option) of counterexamples. You can watch the diagnostic trace in the Simulator.
• You can check if it possible to deadlock your system be writing: A[] not deadlock in the Verifier.
• If you want to use the Person automaton in the figure above (which is suggested) you need to modify it somewhat since it is not a exactly a correct Uppaal automaton. You have to replace the y=3 statement with y==3 and the y=2 statement with y==2. You must rename one of the two Wait states since all names must be unique in Uppaal.
• To get a correct behaviour from your system you need to declare all the communication channels, ie. coin, cof and coin, as urgent, (ie. as urgent chan coin). This will ensure that a transition is taken as soon two interacting automata are ready to synchronise. Please observe that you can not have any clock guards on transitions which are synchronizing over channels that are declared as urgent. You don't need to declare any states as urgent or committed.
• UPPAAL allows you to create either global variables (accessible by all automata) or local variables (only accessible by one automaton). If you want to see how the global time proceed, declare a global clock which you never reset.
• Before you save your model it is a good idea to check the syntax using the Check Syntax option in the File menu.
• If you want to reuse the Person automaton (eg. for creating several PhD students) you should create the automata as a template. In the process instantiation declaration you create a Phd student instance as: PhDStudent := Person() or a coffee machine instance like: CoffeeMachine := Machine(). Then in the System definition declaration you declare the processes that is part of your system as: system PhdStudent, CoffeeMachine;.

A Simple Protocol

The main purpose of this assignment is to practice modelling of a protocol with some real-time properties, and to get more familiar with the simulation of models.

You are asked to model a communication medium M, a Sender, and a Receiver.

The sender sends messages of a fixed length length, which is the time between the beginning and the end of a message. The medium has a transmission delay delay, which is the time between the beginning (or end) of a message is sent and the beginning (or end) of a message is received. For example, if the beginning of a message is sent at time t, it will be received by the receiver at time t+delay.

Task 1: Model the system as a network of timed automata in UPPAAL. Assume length<delay. Model the beginning and end of each message. It is recommended to use integer constants in UPPAAL for the values length and delay.

The medium automata should not be needing the length value to work correctly. Instead it only needs synchronize with the other two automata using the b = begin send, e = end send, br = begin receive and er = end receive communication channels.

Task 2: Validate the system in the simulator and find out what the total timed between begin send and end receive is.

Task 3: Extend the medium M to also handle messages of length length>=delay.

The Gossipping Girls Problem

The main purpose of this assignment is for you to see how scheduling problems can be solved by reachability analysis.

Model and analyze the following gossipping girls problem in UPPAAL. 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 (between two girls in each phone) calls should be possible.

Use UPPAAL to find the minimal number of phone calls needed for four girls to know all secrets. Also give an example schedule for the calls between the girls.

OtionalTask 2: Give an (inductive) argument for the number of phone calls needed to solve the gossipping girls problem for n girls.

Modelling tips:

• UPPAAL allows you to declare arrays like in C. Eg. int a[10]; will declare an array indexable from 0 to 9.
• UPPAAL allows you to create integers with limited value domains. Eg. int[0,1] i will declare an integer which only can have a value of 0 or 1.
• UPPAAL allows you to use a C-like conditional assignment. Eg. max = (a > b ? a : b); will assign the largest value of a and b to max.
• UPPAAL allows you to declare urgent channels which forces a transition to be taken as soon two interacting automata are ready to synchronise.
• The girls will probably be very similar, so declaring them as one Template is good idea.

Working@Home

To work at home you need to download the tool from the Uppaal website: www.uppaal.com. In addition you need to have version 1.4 or better of Java Runtime Environment (JRE) or Software Development Kit (SDK) installed. There are several implementations of Java, for example Suns at java.sun.com

Report

A proper report is to be handed in for the assignment. It should include at least the following:

• The cover page.
• Answers to the given assignments (in part 2 all three task should be presented). These have three parts, the created timed automata, text describing how your timed automata are supposed to work and last (but not least) the verification queries used to answer the question.