Testing synchronous critical software

Three approaches to the problem of testing synchronous critical software are presented, based on the data-flow language LUSTRE. The first approach automatically transforms a set of LUSTRE invariant properties characterizing the environment 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. The usual structure-based testing criteria are adapted to the operator net associated with the LUSTRE nodes. Moreover, an automatic test data generation process is described for this last approach using LESAR, a tool designed to automatically prove the satisfaction of safety properties on LUSTRE programs