Verification 5

Subject

Real Time Modelling. Timed Automata. UPPAAL

Material

AD + JPK chapter 1, chapter 4 till section 4.3.
UPPAAL (i.e. UPPAAL in a Nutshell).
LSW.

Exercises

Exercise 1 (a nice warm-up)

 

In this exercise you are asked to design the control of a Machine (the control program) which will serve a coffee craving Person (the environment).  As you can see (click here for a better view) 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.

The machine takes some time for brewing the coffee and will  time-out if 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 experiences a constant flow of publications from the system.  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.  Try to determine the maximum brewing time allowed by the Machine in order that the above requirement is met.

 

Exercise 2

Reconstruct a model of the Smart Light Swithch (Intelligent Light Control) from Lecture 2 taking timing into account.  Below you see (from the lecture) a timed automata model of the interface between the user and the control program.  Complete the model by designing appropriate automata for the control program.  Simulate the model and try to estimate the minimum time to take the light to its maximum intensity.  You can find a draft of the model here (with stubs for the user and the control program).

 Exercise 3

Consider the above system, where a SENDER and a RECEIVER wants to communicate over a potential faulty communication line.  In order to allow the SENDER to detect when communication succeeds, two (potentially faulty) communication media are used: one (K) for transmitting the message from SENDER go RECEIVER and one (L) for transmitting acknowledgements from the RECEIVER to the SENDER.  We assume that the both media are one-place buffers.  Also, we shall pay no attention to the actual message being communicated.

Use UPPAAL to model and analyse communication systems of the above type, where the media

               are lossy
               have delays

The desired behaviour of the overall system is that of a one-place buffer.  Use UPPAAL to examine to what extent this behaviour is meet in the various scenarios above.