Using on the fly verification techniques for the generation of test suites.

CAV'96, Conference on Computer Aided Verification
July 30 - August 3
Rutgers University, New Brunswick, New Jersey, USA

Paper (PostScript 70K)

Slides (PostScript 143K)

Jean-Claude Fernandez, Spectre/Vérimag/Inria/Grenoble
Claude Jard. Pampa/IRISA/CNRS
Thierry Jéron. Pampa/IRISA/INRIA/Rennes
César Viho. Pampa/Irisa/Université/Rennes

Conformance testing is one step in the validation process in which one checks for the conformance of an implementation under test (IUT) with respect to a specification. We deal here with what is called black box testing in which a tester can only interact with the implementation by inputs and outputs. The main difficulty of the testing activity is to generate interesting test suites (i.e. sets of test cases) which verdicts increase the confidence in implementations or reject them. In this paper we attempt to demonstrate that on-the-fly techniques, developed in the context of verification, can help in deriving test suites. Test purposes are used in practice to select test cases according to some properties of the specification. In a way quite similar with the verification activity, we advocate the use of formal test purposes and we define a consistency preorder linking test purposes and specifications. We define a conformance relation linking specifications and implementations, which distinguishes inputs of the environment, which are observable by a tester, from outputs, which are controlable. We describe a system of formal rules which inputs are a test purpose and a specification and which checks for consistency while deriving a complete test case with preamble, postamble, verdicts and management of timers. We prove that test cases derived by those rules are sound (an implementation which conforms the specification is never rejected) and exhaustive (an implementation which does not conform the specification can be detected under a fairness assumption). We then describe an algorithm which implements the construction rules by a depth first traversal of a kind of synchronous product between the test purpose and the specification. This algorithm is an on-the-fly algorithm i.e. it can be run during the construction of the state space of the specification. We then shortly relate our experience on an industrial protocol with a first prototype of the algorithm, named TGV and implemented as a software component of the CADP toolbox.