Real-Time Systems

Lecture 6

Subject

Symbolic Reachability Checking
From Reachability to Bounded-Liveness Properties
Abstraction and Simulation as Reachability

Material

Slides.
UPPAAL in a Nutshell sections 4.2 and 4.3
Cormen, Leiserson and Rivest: Algorithms,  section 25.5
J Bengtsson and F Larsson: UPPAAL a Tool for Automatic Verification of Real-Time Systems. pages 26-40.
                The full version can be found on UPPAAL's homepage.

Exercises

Exercise 1

Finish the modelling of the Gossiping Girls Problem in UPPAAL (if you have not already done so).  In particular make sure that you deal with the timed version of the problem, i.e. task 3 from last time.

Task 3: Refine your model so that each phone call requires start time units to connect, and in addition
   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.
 

Exercise 2

This exercise will (hopefully) convince you that reachability checking in the UPPAAL-model is a hard problem indeed (NP-hard); if fact consider how you could use UPPAAL to analyse satisfiability of propositional logic formulas, i.e. formulas F build from propositional variables,  b1, b2, b3,...... using boolean connectives (and, or, negation, ....).   You may assume that F  is in conjunctive normal form that is

F   = C1 and C2 and C3 and ....... and Cn,         where
Ci   = Li1  or Li2   or Li3  or ......... or Lik,            where
Lij  is a variable   bi   or a negated variable   ~bi

Apply your idea for a construction to the formula:

(x or y or ~z or u)  and  (~x or y or z or ~u)  and ( x or ~y or ~z)  and  (~x or y or ~u)

to see if the formula is satisfiable and if so to obtain a satisfying assignment to the boolean variables x, y, z and u.
 

Exercise 3

The reachability algorithm of UPPAAL is based on efficient representation and manipulation of Difference Constraints Systems, i.e. linear equation systems between clock values where each constraint is of the simple form   (x_j - x_j) <= b_k.   In this exercise you should think about how to  use UPPAAL to decide whether a given difference constraint system has solutions or not.  Use your method to decide whether the following systems have solutions or not.  In case there are solutions try to use UPPAAL to exhibit a single solution:

System 1:  x1-x2<=1, x3-x1<=-1,  x1-x4<=3, x2-x3<=5.

System 2:  x1-x2<=1, x1-x4<=-4, x2-x3<=2, x2-x5<=7, x2-x6<=10, x4-x2<=2, x5-x1<=-1, x5-x4<=3, x6-x3<=-8.

Consider also how to use UPPAAL to check for two difference constraint systems D1 and D2 whether all solutions to D1 are also solutions to D2.  Use your 'method' to check whether the constraint system 1 above is included in the following system 3:

System 3: x1-x3<=7, x3-x4<=2,  x3-x2<=4.
 

Exercise 4

 

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).