geteta — Generalized Test Tables

Generalized Test Tables ensures safety in automation software.

• Authors:
  • Alexander Weigl [email protected]
• License: GPL v3

Download

• 0.6.0: not released yet
  • omega duration
  • wait duration
  • Reintroduction blocks
  • Empty cells copies has the value from the cell above. If no cell above (first row), it is don't-care -.
• 0.5.0-alpha: not released
  • new automata model
  • different verification techniques (IC3, BMC, LTL)
• 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 element.

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

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.

Featured

• gotos
  • conditionals
• User-defined integer bit widths
• CI tests with nuxmv
• load options via a properties file