KIT Logo - Link to KIT start page
Application-oriented Verification
Karlsruhe Institute of Technology

geteta — Generalized Test Tables

Codacy Badge CircleCI

Generalized Test Tables ensures safety in automation software.


These are jar files include all dependencies:

From Source

$ git clone
$ 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 -t testtable.xml [-x]

Command Line Arguments

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.


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.


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



Name Description
identifier variable identifier
io input or output
data-type IEC61131-3 builtin datatype. Currently supported: AnyInt and AnyBit


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


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

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.

Additionally, we introduce abbreviations.

A simple constant means the equivalence with this value.

5 means X = 5 and FALSE is NOT X.

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.

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).

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 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

The mode of test tables has following effect:

Cycles through the steps

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

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


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