Verification 5

Time:   25. May 2001

Litterature:

• (**) JPK chapter 4.
• (*)  Larsen, Pettersson, Yi: "UPPAAL in a Nutshell", in Journal for Software Tools for Technology Transfer, vol 1, 1997.
• (*) Rajeev Alur, David Dill: "Automata for Modeling Real-time Systems", in Proceedings of ICALP90.
• (*)   Rajeev Alur, Costas Courcoubetis, David Dill: "Model-Checking  for Real-Time Systems", In Proceedings of LICS90.
• (*)   Larsen, Steffen, Weise: "Continuous Modelling of Real Time and Hybrid Systems", in Journal for Software Tools for Technology Transfer, vol 1, 1997.
• (*)   Yi, Pettersson og Daniels: "Automatic Verification of Real-time Communicating Systems by Constraint-Solving", in proceedings of FORTE94.

• Slides from Estonian Winter School on Computer Science can be found here.

• Slides from MFPS can be found here (.ppt).

Excercises:

Exercise 1 (as a warm-up):

Experiment with the BRICK Sorter model (.xta, .ugi) in UPPAAL.

Change the model so that the control task TaskMAIN and the bricks communicate via a shared interface (integer) variable IN_1.

Change the (model) of the control tasks so that sorting is now based on length of bricks rather than color, i.e. we want (say) long bricks to be kicked off wherea short bricks should be go straight through the sorter.

Change the model of the controlling tasks (you may choose either the color-sorting or the length-sorting version) so that it works correctly even in cases when two black/long bricks are simultaneously on the belt.

Exercise 2 (to be handed-in):

Experiment with the various verification options of UPPAAL on Fischers Protocol (.xta, .ugi, .q)  and The Soldiers Problem (.xta, .ugi,.q). Estimate the verification times required and try to conclude on which options are to be prefered on which examples.

Construct an example where use of the verification option 'Over-approximation' gives the wrong answer.  Try to make your example as small as possible.

Exercise 3 (to be handed-in):

In this exercise you are asked to develop and implement a list-based datastructure which allows regions to be represented and manipulated as required when constructing the region automata of a timed automata.  You can find the detailed description of the assignment here (.ps, .pdf).

Exercise 4 (very optional - maybe Oliver wants to have a look):

Baggage Sorting Facility -- modelling and verification assignment using UPPAAL posed at DTU  spring 2001 (.ps, .pdf).

Exercise 5 (extremely optional - just for information).

Production Cell -- modelling and verificaiton assignment using UPPAAL posed at DTU spring 2000 (.html).

Kim