Automatic Test Generation for LUSTRE/SCADE Programs

Lustre is a declarative, data-flow language, which is devoted to the specification of synchronous and real-time applications. It ensures efficient code generation and provides formal specification and verification facilities. A graphical tool dedicated to the development of critical embedded systems and often used by industries and professionals is SCADE (Safety Critical Application Development Environment). SCADE is a graphical environment based on the LUSTRE language and it allows the hierarchical definition of the system components and the automatic code generation. This research work is partially concerned with Lutess, a testing environment which automatically transforms formal specifications into test data generators.