Relational test tables: A practical specification language for evolution and security

Alexander Weigl, Mattias Ulbrich, Suhyun Cha, Bernhard Beckert, Birgit Vogel-Heuser
[arXiv] [Google Scholar] [DBLP] [Citeseer]
Read: 11 August 2020

arXiv 1910.09068 cs.LO
Note(s): test generation, information flow, kripke structure, model checking, unit tests

Relational test tables describe sets of traces and constraints on those traces and (the relational part) between traces and support for stuttering (to allow for timing differences).

Extends authors previous work that generalized “concrete test tables” to support verification by replacing concrete input values with constraints.

They target reactive systems so test tables describe sequences of inputs and outputs with timing constraints.

Compare with approaches from the model checking community based on Kripke structures.

Implementation uses nuXmv and IC3 model checkers and demonstration is based on a Pick and Place Unit (PPU).