Next: Formal Methods in Model-Based Design
- Polyspace® and Prover Plug-In® formal analysis engines
- Detection of dead logic, integer and fixed-point overflows, division by zero, and violations of design properties
- Blocks and functions for modeling functional and safety requirements
- Test vector generation from functional requirements and model coverage objectives, including condition, decision, and modified condition/decision (MCDC)
- Property proving, with generation of violation examples for analysis and debugging
- Fixed-point and floating-point model support
Simulink Design Verifier enables you to perform model analysis within the Simulink® environment. It lets you verify your designs and validate requirements early without having to generate code. As a result, you can perform verification and validation throughout the design process. Model analysis with Simulink Design Verifier complements simulation by letting you use simulation results as inputs to analysis with formal methods.
Simulink Design Verifier supports the discrete-time subset of Simulink and Stateflow® typically used in embedded control designs.
Design error detection in a model using Simulink Design Verifier. The block highlighted in red has a design error; the subsystem highlighted in green is proven correct.