In the following we give a pseudo-formal semantics for the requirement specification language of UPPAAL. We assume the existence of a timed transition system (S, s0, →) as defined in the semantics of UPPAAL timed automata. In the following,
q are state properties for which we define the following temporal properties:
See also Syntax of Symbolic Queries.
E<> p evaluates to true for a timed transition system if and only if there is a sequence of delay and action transitions s0 → s1 → … → sn, where s0 is the initial state and sn satisfies p.
A p evaluates to true if (and only if) every reachable state satisfy
An invariantly property
A p can be expressed as the possibly property
not E<> not p.
E p evaluates to true for a timed transition system if and only if there is a sequence of delay and action transitions s0 → s1 → … → si → … for which p holds in all states si and which either:
A<> p evaluates to true if (and only if) all possible transition sequences eventually reaches a state satisfying
An eventually property
A<> p can be expressed as the potentially property
not E not p.
p --> q denotes a leads to property meaning that whenever
p holds eventually
q will hold as well. Since UPPAAL uses timed automata as the input model, this has to be interpreted not only over action transitions but also over delay transitions.
A leads to property
p --> q can be expressed as the property
A (p imply A<> q).
Any side-effect free expression is a valid state property. In addition it is possible to test whether a process is in a particular location and whether a state is a deadlock. State proprerties are evaluated for the initial state and after each transition. This means for example that a property
A i != 1 might be satisfied even if the value of
i becomes 1 momentarily during the evaluation of initializers or update-expressions on edges.
Expressions on the form
P is a process and
ℓ is a location, evaluate to true in a state (L, v) if and only if P.ℓ is in L.
The state property
deadlock evaluates to true for a state (L, v) if and only if for all d ≥ 0 there is no action successor of (L, v + d).
The UPPAAL requirement specification language supports five types of properties, which can be reduced to two types as illustrated by the following table.
not E<> not p
not E not p
p --> q
A (p imply A<> q)