Requirements Specification

This section describes a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.

Symbolic Queries

Symbolic queries are performed using symbolic operations based on symbolic semantics of timed automata and correspond to a mathematically rigorous proof.

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

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

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

List ::= Expression | Expression ',' List

For sup properties, expression may not contain clock constraints and must evaluate to either an integer or a clock.

See also: Semantics of the Symbolic Queries

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.

Controller Synthesis Queries

Controller synthesis queries are decided using symbolic techniques over Timed Game (TIGA) automata, where the discrete actions are either controllable (controller’s actions, solid edges) or uncontrollable (environment actions, dashed edges). The result is either a strategy solving the game objective or that the strategy does not exist.

TIGAQuery ::=
        'control:' 'A<>' WinExpression
      | 'control:' 'A[' NotLooseExpression 'U' WinExpression ']'
	  | 'control:' 'A[' NotLooseExpression 'W' WinExpression ']'
      | 'control:' 'A[' NotLooseExpression ']'

WinExpression ::= Expression

NotLooseExpression ::= Expression

Statistical Queries

Statistical queries are decided using concrete semantics of stochastic hybrid automata over a number of bounded concrete simulation runs and correspond to empirical measurements of the system performance. The results are of statistical estimate nature and may vary across different executions based on uncertainties specified in the statistical parameters.

SMCQuery ::=
	  | Simulate
      | Probability
      | ProbUntil
      | Probability ( '<=' | '>=' ) PROB
      | Probability ( '<=' | '>=' ) Probability
      | Estimate

Simulate ::= 'simulate' '[' SMCBounds ']' '{' List '}' [ : Expression [ ':' SATRUNS ]]

Probability ::= 'Pr[' SMCBounds ']' '(' PathType Expression ')'

ProbUntil   ::= 'Pr[' SMCBounds ']' '(' Expression 'U' Expression ')'

Estimate ::= 'E[' SMCBounds ']' '(' ('min:' | 'max:') Expression ')'

SMCBounds ::= BoundType [ ; RUNS ]

BoundType ::= (  | Clock | '#' ) '<=' BOUND

PathType ::= ( '<>' | '[]' )

BOUND

is a non-negative integer constant denoting an upper bound over the absolute global time (when a variable is not specified), specific Clock (cost) variable or a number of action-transitions (#).

RUNS

is an optional positive integer constant denoting the maximum number of runs. If the number of runs is not specified, then it is decided based on statistical parameters and the particular estimation algorithm.

SATRUNS

is an optional positive integer constant denoting the maximum number of runs that satisfy the state expression.

PROB

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

'#'

means a number of simulation steps -- discrete action-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.

See also: Semantics of the SMC Queries

Learning Queries

LearningQuery ::=
     ExpQuantifier '(' Expression ')' '[' BoundType ']' Features ':' PathType Expression

ExpQuantifier ::= ( min | max )

Features ::= '{' List '}' '->' '{' List '}'

Features

describes a mapping from partial state to .

Strategy Queries

Strategy queries allow store, load, reuse and refine the strategies by assigning names to them.

StrategyQuery ::=
	    'strategy' Name '=' Query [ 'under' Name ]
	  | 'saveStrategy' '(' Path ',' Name ')'
	  | 'loadStrategy' Features '(' Path ')'

Query ::=
        SymbQuery
	  | TIGAQuery
	  | SMCQuery
	  | LearningQuery

Path

is a double-quoted character sequence (string) denoting a file system path.