Types and Expressions in ALISA

ReqSpec allows the user to introduce typed variables and specify predicates using an expression notaiton. Similarly, Verify allows users to specify formal parameters for verificaiton methods and actual parameter values to be used when verification activities call verificaiton methods. This section provides details on how to specify types and expressions.

Specifying Types

The types of variables and formal parameters can be numeric values with an optional measurement unit, numeric value ranges, as well as Booleans, strings, references to model elements, and values of any user defined property type. Acceptable measurement units are any unit defined as Units literals in property sets of the AADL core language.

TypeSpec ::= BaseType | typeof <PropertyName>
BaseType ::= boolean | string | integer (units <UnitsTypeName> )?

| real (units <UnitsTypeName> )? | model element | <PropertyTypeName>

Users can introduce new types through the property sublanguage of AADL by defining new property types. They can also use predeclared property types that come with the AADL V2.2 standard.

Expression Notation

This section describes the initial expression notation support for ReqSpec and Verify in the OSATE 2.2.1 maintenance release of May 2015. The expression notation will be aligned with the emerging AADL Constraint Annex.

It supports the specification of value predicates in ReqSpec and of actual parameter values in calls to verification methods in verification plans expressed in Verify.

The expression notations allows for reference to constants and compute variables defined in ReqSpec, to properties in the AADL model,literals of the various types, as well as references to model elements.

Operators and their precedence in expressions

Primary expressions:

1. Unit operations for numeric expressions

a. Unit assignment to a unit-less expression
<primary expression> <unit name>
Example: (x + 1) ms, where X is an integer or real value without a unit.

b. Conversion to numeric value without unit
<primary expression> in <unit name>
Example: (2.0ms) in ns, evaluates to 2000

c. Conversion to different unit
<primary expression> % <unit name>
Example: (2ms) % ns, evaluates to 2000ns

2. Conditional expression
if <Boolean> then <expression1> else <expression2> endif
Both expression1 and expression2 must have the same type.

3. Reference to model element
this.<element name>.<element name>. … .<element name>
The keyword this refers to the target classifier of the requirement or requirement set.

4. Reference to property value in model
<model element>#<property name>
#<property name> (short form of this#<property name>)
The property name must be a property or a property constant, the model element must be either a literal model element reference or a value of type model element.

5. Reference to ReqSpec constants and computed variables by variable name. For example, a user specifies ActualCPUBudget <= MaxCPUBudget, where MaxCPUBudget is a constant and ActualCPUBudget is a computed variable.

6. Literals with examples

a. Boolean literal: true, false

b. Integer literal, optionally with unit: 2000, 20ms

c. Real literal: 12.5, 2.5ms

d. String literal: “strings are enclosed in double quotes”

e. Range literal: [1 .. 5], [500ms .. 2s]
Note that a space character is needed before the two dots.

6. Automatic type conversion between Real and Integer occurs to match the target type. For example users can assign an Integer value (numeric value without decimal point) to a constant of type Real. Similarly, addition of an Integer value and a Real value results in a Real value.

7. Built-in functions: the following built-in functions are supported

a. min, max: minimum or maximum value of a range

b. abs: absolute value

c. floor, ceil, round: next lower, higher, closest Integer value for a given Real value

Two functions have been provided experimentally: prev for referring to the previous value, and atTime for referring to a value at time x (second parameter).