Absence Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], it is never the case that P [holds] [Time]
• Pattern Intent: This pattern describes a portion of a system's execution that is free of certain states [within a time-constraint].

State-Based Pattern

Untimed

Globally

Using a formula: A[] not P

Alternative using the observer technique

with A[] not ERROR

The branch from the committed initial state checks whether P holds initially or not. As an alternative to this branch, the property A[] INIT imply not P can be checked so that the branch can be omitted in the observer.

Before R

with A[] not ERROR

The original property is violated if P is reached before R. In this case, the observer is in state ERROR, which should not happen. The original property is not violated in two cases: (1) P is reached and R is not reached afterwards. (2) R is reached before P. In the latter case, reaching R before P closes the scope such that afterwards anything may happen (even reaching P).

We may explicitly check for A[] INIT imply not R to verify whether the scope is initially open and not closed. However, this is already captured by the guards of the transitions leaving the state INIT.

After Q

A[] Q_held_once == 1 imply not P

In other words, the original property is violated if E<> Q_held_once == 1 and P holds.

Alternative using the observer technique

with A[] not ERROR.

Between Q and R

with

A<> Observer.INIT imply Q and R // warning
A[] not ERROR

The warning property shows if for each path a situation occurs, in which the observer will infinitely loop between the INIT location and the following committed location.

Comment: Using the flag technique here (in general for the scopes Between Q and R and After Q until R) is more complicated since the variables cannot just be set when reaching or leaving a state. In contrast, the setting of a variable depends on other variables or on the relative order when the states are reached or left. Moreover, the flag technique does not work here since we cannot distinguish the case whether state R will eventually be reached or not. Therefore, the observer technique seems to be more intuitive.

After Q until R

with

A<> Observer.INIT imply Q and R // warning
A[] not ERROR

Timed

Globally

A[] ((gc >= t1 and gc <= t2) imply not P)

where gc is a global clock added to the system model, t1 is the lower and t2 the upper time bound. Thus, when the time constrained is satisfied, the system must not be in state P.

If t1 or t2 are not set by the user, we can skip the respective part of the property: A[] (gc >= t1 imply not P) respectively A[] (gc <= t2 imply not P), or set them to defaults, t1 to 0, and t2 to the max integer value that UPPAAL can handle.

Alternative using the observer technique:

with

A[] (INIT and c == t1) imply not P
A[] not ERROR

or

with A[] not ERROR.

Before R

with A[] not ERROR.

Note: We consider the case when R holds or is reached before t1 as an error. To check that R does not held initially, we can check A[] INIT imply not R instead of the the branch leaving the INIT location.

After Q

with A[] not ERROR.

Alternative

A[] INIT imply not Q
A[] (SCOPEOPEN and c == t1) imply not P
A[] not ERROR

Between Q and R

with

A<> Observer.INIT imply Q and R // warning
A[] not ERROR

After Q until R

with

A<> Observer.INIT imply Q and R // warning
A[] not ERROR