Sabrina von Styp-Rekowski

 

 

Towards a Testing Theory for Timed and Symbolic Systems




Abstract:

Model based testing is one of the most promising techniques for
automatic testing. It allows the automatic derivation of test cases
from a formal model (e.g. labelled transition systems, timed automata,
etc.) describing the system under test. A well-know representative of
model based testing is the ioco-theory using labelled transition
systems as models and a conformance relation to formally define when
the implementation relation conforms to its specification. Based on
the ioco-theory there exists several extensions such as tioco for
timed labelled transitions systems and sioco for symbolic transition
systems. This thesis introduces two implementation relations for
systems combining symbolic and timing behaviour. The relation is
called tsioco and is defined for timed symbolic transition system, a
formalism which allows concrete delay transitions for symbolic
transition systems. The second implementation relation is stioco_D for
symbolic timed automata. It combines the tioco and the sioco
implementation relation to systems with data and real-time behaviour
and allows interaction between time and data. We choose a purely
symbolic approach to define this relation, which is based on similar
work of Frantzen et al. for Symbolic Transition Systems. We show that
stioco_D and tsioco correspond to the implementation relation tioco,
defined by Krichen and Tripakis.