As safety critical systems increase in size and complexity, the need for efficient tools to verify their reliability grows. In this paper we present a tool that helps engineers design safe and reliable systems. Systems are reliable if they keep operating safely when components fail. Our tool is at the core of the Scade Design Verifier integrated within Scade, a product developed by Esterel Technologies. Scade includes a graphical interface to build formal models in the synchronous data-flow language Lustre. Our tool automatically extends Lustre models by injecting faults, using libraries of typical failures. It allows to perform
Failure Mode and Effect Analysis
, which consists of verifying whether systems remain safe when selected components fail. The tool can also compute minimal combinations of failures breaking systems’ safety, which is similar to
Fault Tree Analysis
. The paper includes successful verifications of examples from the aeronautics industry.