SYRF Project

Task 3.5: "Use of automata technology and synchronous observers for automatic testing"

Abstract of deliverable 3.5.1

Back to the SYRF Home Page



Approach:

Testing will remain an important validation technique, especially in the cases where formal verification fails, i.e., 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.