geteta — Generalized Test Tables

Generalized Test Tables ensures safety in automation software.

• Authors:

  • Alexander Weigl weigl@kit.edu

• License: GPL v3

Getting Started

Download

These are jar files include all dependencies:

• 0.5.0-SNAPSHOT: not released

  • new automata model
  • different verification techniques (IC3, BMC, LTL)
  • latest useable version for `stvs <../stvs/index.md>`__

• 0.4.4: geteta-0.4.4-exe.jar

  • Fix a bug in the clocks.

• 0.4.3: geteta-0.4.3-exe.jar

  • Change clock initial value to 1 as off-by-one error

• 0.4.2: geteta-0.4.2-exe.jar

  • Kills nuXmv, if geteta is killed
  • depends on new version of iec61131lang

• 0.4.1: geteta-0.4.1-exe.jar

  • bug fixes: missing constraint on free variables are treated as don’t cares

• If a free variable is an enum, every allowed enum literal is allowed (super-enum to rule them all).

• 0.4.0: geteta-0.4.0-exe.jar

• Counter examples in the semantic of traces in the test table

  • 0.3.0: geteta-0.3.0-exe.jar

• enum support tested and fixed

  • 0.2.2-beta: geteta-0.2.2-beta.jar

• better nuxmv output parser

  • 0.2.1-beta: geteta-0.2.1-beta.jar

• Internal changes

  • 0.2.0: geteta-0.2.0.jar

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

<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

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

Additionally, we introduce abbreviations.

• 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

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