Real-Time Systems

Lecture 7

Subject

UPPAAL verification directives
    Active Clock Reduction
    Local/Global Reduction
    Reuse of State-Space
    Over-approximation (Convex Hull)
    Under-approximation (bit-state hashing)
    and other techniques for dealing with state-space explotion.

Presentation of Project

Material

Slides (UPPAAL's verification directives)
Slides (Project Assignment)

JPK sections 5.2, 5.4.

C. Daws and S. Tripakis:
    Model checking of real-time reachability properties using abstractions.
    In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'98,
    LNCS 1384, 1998.

Fredrik Larsson, Paul Pettersson, and Wang Yi.
   On Memory-Block Traversal Problems in Model Checking Timed Systems.
    To appear in Tools and Algorithms for The Construction and Analysis of Systems 2000.

Exercises

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

Exercise 2 (Over-Approximations)
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 (Active Clock Reduction)
Consider the timed automaton below:

Calculate the active clocks for the three locations, S0, S1 and S2.  Compute the reachable symbolic state-space of the timed automaton (using canonical DBM's for representing constraint systems) first without any reduction and afterwards with 'Active-clock reduction'.   Compare the number of constraints and symbolic states required  to represent the reachable state-space in the two cases.
 

Exercise 4 (Pending from last time for most of you)
 

Consider the two timed automata P1 and P2 above.   The automata are interacting over an urgent channel a.  Use the testautomata or decoration technique for analysing bounded liveness properties of the form:

• whenever P1.S1 then P2.S0 within t  timeunits,
• whenever P1.S0 then P2.S4 within t  timeunits,
• whenever P1.S0 then P2.S0 will not occur before t timeunits.

You can find downloadable version of the system here (.xta, .ugi).

---

EVALUATION of UPPAAL

We would be most grateful if you would take a few minutes to answer the following questions.
In all cases try to comment on both positive and negative experiences with the tool.
 

1. How easy was it to get started using UPPAAL?

 

 
 
 
 
 

2. How easy was it to install the tool (if you installed it on your own machine)?

 

 
 
 
 
 

3. On which platform did you install UPPAAL

 

 

        - which Java version have you been using?

        - which operating system?

        - CPU  and RAM?
 
 

4. How useful do you find the on-line documentation?

 

 
 
 

5. How did you find the User Interface

 

 

        - of the simulator?

        - of the editor?

        - of the verifier?
 
 

6. Comment on the stability of UPPAAL.

 

 
 
 

7. What did you like about the tool (list your 3 top-favorites)?

 

 
 
 

8. What did you NOT like about the tool (list the 3 features your disliked the most)?

 

 

9. Did you find the examples in the demo directory  useful (or do think we should include some of the examples you have dealt with in the course)?

 

 

10. Did you consult the UPPAAL homepage and if so do you have any comments/suggestions for improvement?

 

 

11. Do you have any other comments?

 

 
 
 

Please give Paul your answers before you leave!!

---