Testing Techniques for Data-Flow Synchronous Programs

Three approaches to the problem of testing synchronous data-flow programs written in LUSTRE are presented. LUSTRE is a language well-adapted to both the specification and the development of reactive software. The first approach automatically transforms a set of LUSTRE invariant properties characterizing the environment of the reactive program into a constrained random generator of test data sequences. The second approach consists in analyzing the required safety properties (written in LUSTRE) of the software. This analysis may result, in specific cases, in automatic generators of relevant test data. The third approach considers that LUSTRE is used for the implementation of the software, and defines structure-based testing criteria. These criteria are specific to the model which captures the LUSTRE program structure : the operator net. Moreover, an automatic test data generation process is described for this last approach using LESAR, a tool designed to automatically prove the satisfact..