Mutation Analysis for Reactive System Environment Properties

Reactive systems used in safety-critical domains demand high level of confidence. The development of these systems, which are submitted to several normative recommendations, is complex and expensive. Reactive systems can be developed by using the data-flow approach: many languages support this approach such as MATLAB/SlMULINK, LUSTRE/SCADE. This paper concentrates on the LUSTRE/SCADE language, especially the description of reactive system environment properties in this language. The description of environment properties, which is important for the validation (the proof and the test) of reactive systems, is not easy. Hence, we would like to use the mutation technique to consolidate this difficult task: we use the LESAR model-checking tool to detect equivalent mutants and some test case generators such as GATEL or LUTESS tools to kill non-equivalent mutants.