Testing will remain an important validation technique, especially in the
cases where formal verification fails, i.e.,
for programs with significant numerical aspects
for programs the source code of which is not fully available -
either because it is partly written in languages which are not supported
by verification tools, or because they are implemented by hand (in
particular on distributed architectures).
Our approach consists in using synchronous observers, already used
in verification, to describe: The expected behavior of the program, in order to allow testing
diagnosis ("oracle") to be automatically generated; The known properties of the environment, in order to avoid
the generation of unrealistic test cases. The test objectives, by which the user can concentrate the test
on some classes of scenarios.
Achieved Results:
A testing tool, called LURETTE, is under development at
INRIA/Spectre. The available prototype is devoted to observers written
in LUSTRE, and contains the following components: A test case generator, which, from a set of assumptions and
objectives described by an observer written in LUSTRE, automatically
generates test sequences. This tool takes into account both control and
numerical aspects (restricted to linear algebra). A test bed, which uses the industrial code generator
developped by VERILOG to run the program under test together with the
test case generator. An "oracle": The pair generator/program can be
connected with an observer of the expected behaviour, which decides
on-line whether the observed sequence of inputs/outputs fulfills the
requirements.
The test cases generator uses
binary decision diagrams (BDDs), for the logical aspects, and
convex polyhedra, for the numerical part.