Esterel Technologies>Products>SCADE Suite>Design Verification

Ensuring design correctness with Design Verifier*

SCADE Design Verifier is a powerful formal proof engine within the SCADE tool. Design Verifier (DV) uses formal methods and makes them efficient even for new users. Because the formal verification capability is encapsulated within SCADE there is no need to learn a new language or a new tool to use this sophisticated and advanced technology.

Design Verifier is used to prove the properties of a SCADE design. It enables you to prove that a design is safe with respect to its requirement. DV can prove that something "bad" will never happen or that something "good" will always happen. DV is instrumental for software debugging. For example, it can be used to verify that two designs are identical with respect to the same requirements. The granularity to which Design Verifier is applied can be selected by the user and it can be applied on a completed model, one node, or even on part of a node. This allows you to find bugs very early in your design cycle. The exhaustive proof capability enables designers to find corner case bugs not detectable by other testing means.

• Transparent combination of the most recent proof techniques for model checking
• Verification of safety, security, trust or any other properties expressed with SCADE blocks: real customer designs with many SCADE nodes verified within seconds
• Automatic counter-example production in case of property verification failure
• Using Design Verifier requires no theoretical background

* SCADE Design Verifier is based on the Prover Plug-In. Prover Plug-In is a trademark of Prover Technology AB in Sweden, the United States and in other countries.