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.