Test Generation using Verification

Thierry Jéron
Irisa/Inria Rennes, France
Friday, 16 December, 2005 (All day)

We address the problem of selecting test cases, for testing the conformance of a black box implementation of a reactive system with respect to its specification.. In this talk, we focus on models of infinite state systems represented by automata extended with variables (ioSTS). We first revisit the ioco testing theory of Tretmans, where the conformance relation defining conformant implementations wrt a specification is a partial inclusion of visible behaviors. We then consider test selection using test purposes, which are specified by ioSTS reachability observers, and allow to focus selection on some behaviours to be tested. The goal is to produce an ioSTS test case that checks both non- conformance and acceptance by the test purpose. The problem reduces to co- reachability analysis, which is undecidable for ioSTS. However, we show that an approximated analysis (using e.g. abstract interpretation) still allows to produce sound test cases. An adaptation of the approach can be used to generate test cases that may detect non-conformance and violations of safety properties, on both the implementation and the specification, thus complementing (a potentially partial) verification of safety properties on the specification.