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 Gossiping Girls exercise from last lecture. In particular deal with task 3 focusing
on a timed version of the problem.
As a starting point you may find it useful to consult the following
suggestion for an untimed solution to the problem provided by Paul Pettersson
(.xta, .ugi, .q) (in particular try to also
deal with task 3 focusing on a timed version of the problem), and the simple
communication protocol.
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 (xj - xj) <= bk. 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 (x is a local in each of the automata). The automata are interacting over an urgent channel a. Use the testautomata or decoration technique for analysing bounded liveness properties of the form:
o whenever P1.S1 then P2.S0 within t timeunits,
o whenever P1.S0 then P2.S4 within t timeunits,
o whenever P1.S0 then P2.S0 will not occur before t timeunits.
You can find downloadable version of the system here (.xta, .ugi).