02224 Modelling and Analysis of Real-Time Systems        Spring 2024
Stopwatches in UPPAAL

Since version 4.1, UPPAAL as extended the modelling with stopwathces. More concretely, the possibility to set the rate of a clock variable to 0 in certain states.

Using Stopwatches

The default rate of any clock is 1. The rate may be changed by adding (by conjunction: &&) the following rate constraint to the invariant part of a process state:

x' == <boolean expression>

where x is a clock variable, x' denotes the rate (derivative) of the clock and <boolean expression> is an expression evaluating to 0 or 1.

Unlike the standard part of the invariant, the rate constraint does not have to be satisfied upon entry to the state, but rather is enforced by setting the rate to the value of the expression by the state entry.

For examples, see below.

Pros and cons

Stopwatches extends the expressive power of the language at the cost of rendering the verification undecidable, ie. for some models, the verification may not terminate. Futhermore, the UPPAAL verification engine in some cases handles stopwatches by overapproximation which means that the verification becomes imprecise and may sometimes not be able to verify properties which actually hold.

This is illustrated by two examples:

stopwatch_1.xml

In this example an activity with a duration of 10 time units is stopped for exactly 2 time units, but at an unknown time. For this example, neither the lower nor the upper bound of the termination can be verified correctly.

stopwatch_2.xml

In this example an activity with a duration of 10 units is stopped at a precise time for an variying amount of time. In this case, the upper and lower bounds for termination can be verified correctly.