# geteta — Generalized Test Tables ¶

Generalized Test Tables ensures safety in automation software.

## Getting Started¶

These are jar files include all dependencies:

### From Source¶

$git clone https://github.com/VerifAPS/geteta.git$ mvn package


## Getting started¶

Ensure, that you have installed nuXmv. You need to set the NUXMV environment variable to the nuXmv executable.

export NUXMV=/home/weigl/work/nuXmv-1.1.1-Linux/bin/nuXmv


After this, you can call geteta with:

java -jar geteta-\${project.version}.jar -c program.st -t testtable.xml [-x]


## Command Line Arguments¶

• -x geteta writes the output in an XML format.
• -m <mode>
• -t <table.xml>
• -c <code.st>
• -v (IC3|INVAR|LTL|BMC)

# XML-Format of Generalized Test tables¶

## What is a test table?¶

A test table describe a behaviour of a reactive system by ensuring allowed input and output values for specific time frames.

## Semantics¶

A system is conform to a test table if and only if the system response with the corresponding (after the test table) output sequence given a valid sequence of input values.

## Input format¶

The test tables are serialized into XML, following the scheme of exteta-1.0.xsd <>__. The XML contains three parts under the root entry.

### <variables>¶

These tag contains the two types of variables: i/o and constraint.

#### <variable>¶

Attributes:

Name Description
identifier variable identifier
io input or output
data-type IEC61131-3 builtin datatype. Currently supported: AnyInt and AnyBit
• I/O variables talk about the the input and output variables of the given program.

#### <constraint>¶

Constraint variables (specification variable) are not visible to the program.

Attributes:

Name Description
identifier variable identifier
constraint a valid cell expression
data-type IEC61131-3 builtin datatype. Currently supported: AnyInt and AnyBit

### <region> and <step>¶

The <steps> tag contains the row (<step>) of the test tables. Each row the value of the cells (cell expressions) in the order of the defined i/o variables.

You repeat a bunch of steps, by wrapping them into a region block.

A region and step tag has the duration attribute, which defines how often the step is applied. The duration is an interval [m,n] with constant values for m,n.

### Cell Expression (<cell>)¶

Formally, a cell expression is generated by the grammar <>__. Informally, a cell expression is a boolean expression over the following operators

• arithmetic +, -, *, /
• logical and, or, xor.

The syntax and semantic, e.g. the operator precedence is tight on the definition of Structured Text and SMV (nuXmv). For example, OR and | is allowed for logical or.

• Constants

A simple constant means the equivalence with this value.

5 means X = 5 and FALSE is NOT X.

• Single-sided comparison

A construct with a relational operator, <,<=,<>,=, >=, >, compares the column variable X with the given expression.

Example: <1 means X<1 resp. >=a+2 expands to X>=a+2.

• Interval

You can specify an interval [m,n] to enforce a lower and upper bound for X: m<=X & X>=n.

Example: [x+2, x+4] means (x+2) <= X <= (x+4).

• Don’t-Care

If you don’t want to force a value, you can use “don’t-care” -.

#### Operators with Precedence¶

1. constants and variable names
2. parens () and unary operators ! NOT -
3. point operators MOD % / *
4. Substraction and Addition + -
5. Comparision < <= >= >
6. equality
7. antivalence
8. logical and & AND
9. logical or | OR
10. logical xor xor XOR

#### <options>¶

Options are key-value pairs of the kind <option key="" value=""/>. They give additional information for the processing of the given table.

Currently allowed options:

##### Program mode¶
• Key: mode
• Values: CONFORMANCE or CONCRETE_TABLE or INPUT_SEQUENCE_EXISTS | Controls

The mode of test tables has following effect:

• CONFORMANCE - default Checks the system conformity against the test table. Returns a counter example, iff the system is not compilant against the above semantic.
• CONCRETE_TABLE Returns a counter example, that represents a concrete run through the test table.
• INPUT_SEQUENCE_EXISTS The above semantics has one problem, if no possible input sequence extension exists. This mode checks if there exists always an input extension.
##### Cycles through the steps¶

In dependence of mode = CONCRETE_TABLE you can give the wanted cycle count for each step.

• Keys: cycles.<id>
• Value: int

where <id> is the number of the region/step (starting with zero, in order of appearance).

##### Data types¶

You can select the bit width of the ST data types. currently not implemented

#### <functions>¶

Between this tag you can define arbitrary function as Structured Text code. These function are usable within the cell expressions as regular function calls.