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