lecturer: Christophe Gaston

We present an approach to test whether a system conforms to its specification given in terms of an Input/Output Symbolic Transition System (IOSTS). IOSTSs are automata based specifications using data types to enrich transitions with data-based messages and guards depending on state variables. We use symbolic execution techniques both to extract IOSTS behaviours to be tested in the role of test purposes and to ground an algorithm of test case generation. Thus, contrarily to some already existing approaches, our test purposes are directly expressed as symbolic execution paths of the specification. They are finite symbolic sub trees of its symbolic execution.

Keywords: Conformance testing, Input/Output Symbolic Transition Systems, Test Purposes, Symbolic Execution, Coverage Criteria.