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

geteta — Generalized Test Tables

Codacy Badge CircleCI

Generalized Test Tables ensures safety in automation software.

Download

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

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

<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

<steps>

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

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

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

Featured