Language specification

A GTL-specification specifies a GALS (globally asynchronous, locally synchronous) system by declaring instances of general models, which are components specified in an external synchronous language (e.g. SCADE). Instances are then connected by fusing outputs of instances to inputs of other instances. Finally, global verification goals may be specified which must hold for the specification to be valid.

Model declaration

A model declaration references a specification of a synchronous component in an external formalism. Syntactically, a model declaration looks like this:

model[<formalism>] <name>(<arguments>) {
  <model_content>
}

Where <formalism> is the name of the synchronous formalism the model is specified in, <name> is the name by which the model can be referenced later and <arguments> is a comma-separated list of formalism-specific options which are used to load the specification of the model. The model content can specify model variables and specify contracts that the model must adhere to.

Interface specification

Variables can be of three different varieties:

Input variables, which specify a port where another component can write data to. For example, the following declares a variable speed of type int:
```
 input int speed;
```
Output variables are variables that will only be written to by the synchronous model.
```
 output int gear;
```
Local variables are not part of the external interface, but can be used in the contract specification, especially in automata contracts.
```
 local int clk;
```

Contracts

Contracts specify how a synchronous component has to behave in order to be considered correctly implemented. Contracts are checked using the synchronous formalism in which they are specified and the contract is used to optimize the model checking procedure for the global verification goals. Contracts are declared with the (optional) keyword contract, followed by a boolean expression that has to hold.

The following contract declares that the output variable gear will always have a value of 5 or less.

contract always gear <= 5;

Cycle-Times

If the timing aspect of components is relevant for the verification goal, it is possible to specify how long a cycle in the synchronous component takes, meaning the time between each operation.

cycle-time 5 ms;

This declares the cycle time to be 5 milliseconds.

Initialization values

To specify the value of input variables before the component supplying the input got a chance to run, default initialization values can be specified. For example, the following sets the initial speed to 15:

init speed 15;

Instance declarations

To create actual components from model specifications, instance declarations are used. The following syntax is used:

instance <model> <name>;

Where <model> is a previously declared model and <name> is the name by which the instance can be referenced.

Connection declarations

A connection between two components can be specified by pairing an output variable with an input variable like so:

connect <instance>.<var> <instance>.<var>;

where <instance> is the name of an instance declaration and <var> is the name of a variable of the interface of the instance. The first variable must be an output variable and the second one must be an input variable. Also, both variables must have the same type.

Verification goals

Verification goals specify properties of the GALS system that the GTL model checker has to prove. They are declared as list of boolean formulas which have to be true for the verification goal to hold.

verify {
  <expressions>
}

The expressions can reference all output variables in the system (connected or unconnected).

Expressions

Expressions can be used to specify contracts as well as verification goals. In a contract, only variables of the interface of the component may be referenced, simply by stating their name, while in the verification goal, only output variables of the components may be referenced by stating the fully qualified name:

<instance>.<var>

Types & constants

As a strongly typed language, expressions in GTL can have the following types:

bool - consisting as usual of the constants true and false
int - 64bit integer numerals
byte - 8bit integer numerals
float - IEEE 754 double precision (64bit) floating point numbers
enum - Enumeration types with a number of different, named values. An enum is declared by enumerating all possible values as:
```
  input enum { red, green, blue } color;
```
Enum-constants are prefixed by a tick ('):
```
  color = 'red;
```
arrays - Arrays contain multiple elements of the same type. In GTL, arrays must be of constant length. They are combined of the type of its elements and the length.

The following code declares x to be an array of ints of length 3:
```
  input int^3 x;
```
Array constants are declared as such:
```
  [2,4,1]
```
tuples - A tuple can contain many elements of different types. Each type is mentioned in the type.

The following code creates an output variable x which is a tuple of an int, a bool and another int:
```
  output (int,bool,int) x;
```
Tuple constants are declared as such:
```
  (3,true,0)
```

Basic logic expressions

Common boolean logic is supported with the operators and, or, =>, and not. Variables and values can be compared using = for equality, != for inequality and >, >=, <, <= with their usual mathematical meaning.

Temporal logic

LTL-style temporal operators are also supported. For example, the following expression states that the property x has to hold until y holds at least once:

x until y

This operator can also be annotated with a time constraint which in the following case specifies that y has to occur within 50 milliseconds:

x until[50 ms] y

If a contract is specified, the time can also be given in cycles (using the time unit "cy").

always states that the following expression has to hold now and in every following step, while finally states that it has to hold somewhere in the future. finally can also be annotated with a time-limit.

To specify that a property must only hold in the next cycle, use the next operator. If it is annotated with a time-property, it means that the property has to hold for the given time-span.

Temporal existential quantification

If a value from the past must be referenced in a contract, one can use existential quantification to do this:

exists v = x: next (x = v)

This specifies for example that the variable x should have the same value in two cycles.

Automata

Instead of specifying a contract with a boolean expression, it might be more convenient to use automata-syntax to specify the behavior of a component. An automaton is declared by using the automaton-keyword:

automaton {
  <states>
};

An automaton is a collection of states. Each state is declared as follows:

initial? state <name> {
  <state_content>
}

If the state is annotated with the keyword initial, the execution of the automaton can start in this state. A state can contain expressions which must be true whenever the state is entered and transitions of the form

transition[<expr>] <target>;

where <expr> is an (optional) expression which must be true if the transition is to be taken and <target> is the name of the state in which the automaton is after it has taken the transition.

Navigation Menu

Repository navigation