Requirements Specification

In this help section we give a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.

Prop ::= 
        'A[]' Expression 
      | 'E<>' Expression 
      | 'E[]' Expression 
      | 'A<>' Expression 
      | Expression --> Expression  

      | 'sup' ':' List
      | 'sup' '{' Expression '}' ':' List  

      | 'inf' ':' List
      | 'inf' '{' Expression '}' ':' List  

      | Probability
      | ProbUntil
      | Probability ( '<=' | '>=' ) PROB
      | Probability ( '<=' | '>=' ) Probability
      | Estimate  

List ::= Expression | Expression ',' List  

Probability ::= 'Pr[' ( Clock | '#' ) '<=' CONST ']' '(' ('<>'|'[]') Expression ')'  

ProbUntil   ::= 'Pr[' ( Clock | '#' ) '<=' CONST ']' '(' Expression 'U' Expression ')'  

Estimate ::= 'E[' ( Clock | '#' ) '<=' CONST ';' CONST ']' '(' ('min:' | 'max:') Expression ')'

CONST

is a non-negative integer constant.

PROB

is a floating point number from an interval [0;1] denoting probability.

'#'

means a number of simulation steps -- discrete transitions -- in the run.

'min:'

means the minimum value over a run of the proceeding expression.

'max:'

means the maximum value over a run of the proceeding expression.

All expressions are state predicates and must be side effect free. It is possible to test whether a certain process is in a given location using expressions on the form process.location. For sup properties, expression may not contain clock constraints and must evaluate to either an integer or a clock.

See also: Semantics of the Requirement Specification Language

Examples

• A[] 1<2
  invariantly 1<2.
• E<> p1.cs and p2.cs
  true if the system can reach a state where both process p1 and p2 are in their locations cs.
• A[] p1.cs imply not p2.cs
  invariantly process p1 in location cs implies that process p2 is not in location cs.
• A[] not deadlock
  invariantly the process is not deadlocked.
• sup: list
  the property is always true and returns the suprema of the expressions (maximal values in case of integers, upper bounds, strict or not, for clocks).
• sup{expression}: list
  The expressions in the list are evaluated only on the states that satisfy the the expression (a state predicate) that acts like an observation.
• The inf formula are similar to sup but for infima. A state predicate should be used when a clock infimum is asked otherwise the trivial result is >= 0.