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, s_{0}, →) as defined in the semantics of UPPAAL. In the following, p and q are state properties for which we define the following temporal properties:
The property E<> p evaluates to true for a timed transition system if and only if there is a sequence of alternating delay transitions and action transitions _s_{0}_→_s_{1}→…→_s_{n}, where s_{0} is the initial state and s_{n} satisfies p.
The property A[] p evaluates to true if (and only if) every reachable state satisfy p.
An invariantly property A[] p can be expressed as the possibly property not E<> not p.
The property E[] p evaluates to true for a timed transition system if and only if there is a sequence of alternating delay or action transitions _s_{0}_→_s_{1}_→…→_s_{i}_→… for which p holds in all states s_{i} and which either:
The property A<> p evaluates to true if (and only if) all possible transition sequences eventually reaches a state satisfying p.
An eventually property A<> p can be expressed as the potentially property not E[] not p.
The syntax 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.ℓ, where 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).
UPPAAL can estimate the probability of expression values statistically. There are four types of statistical properties: quantitative, qualitative, comparison and probable value estimation.
‘Pr[’ ( Clock | ‘#’ ) ‘<=’ CONST ‘](’ ('<>' | ‘[]') Expression ‘)'
Quantitative query estimates the probability of a path expression being true given that the predicate in probability brackets is true. Intuitively the model exploration is bounded by an expression in the brackets: it can be limited by setting the bound on a clock value, model time or the number of steps (discrete transitions).
The result is an estimated probability (with ε confidence interval specified in statistical parameters) and a number of histograms over the values of the variable specified in the probability brackets. Note that histograms omit runs that do not satisfy the property.
‘Pr[’ ( Clock | ‘#’ ) ‘<=’ CONST ‘](’ ('<>’ | ‘[]') Expression ‘)’ ('<='|'>=') PROB
Hypothesis testing checks whether the probability of a property is less or greater than specified bound. The query is more efficient than probability estimation as it is one sided and requires fewer simulations to attain the same level of significance.
‘Pr[’ ( Variable | ‘#’ ) ‘<=’ CONST ‘](’ ('<>’ | ‘[]') Expression ‘)’ ('<='|'>=') ‘Pr[’ ( Variable | ‘#’ ) ‘<=’ CONST ‘](’ ('<>’ | ‘[]') Expression ‘)'
Compares two probabilities indirectly without estimating them.
‘E[’ ( Clock | ‘#’ ) ‘<=’ CONST ‘;’ CONST ‘]’ ‘(’ (‘min:'|‘max:’ Expression ‘)'
Estimates the value of an expression by running a given number of simulations.
The UPPAAL requirement specification language supports five types of properties, which can be reduced to two types as illustrated by the following table.
Name | Property | Equivalent to |
---|---|---|
Possibly | E<> p | |
Invariantly | A[] p | not E<> not p |
Potentially always | E[] p | |
Eventually | A<> p | not E[] not p |
Leads to | p --> q | A[] (p imply A<> q) |