About Systematic Model Verification Using Simulink Design Verifier

Simulink^® Design Verifier™ helps you perform systematic model verification to identify hidden design errors, prove properties, and generate test cases for functional testing. Simulink Design Verifier uses formal methods to test design correctness that increases confidence in your design model that the production code generation uses.

You can perform systematic model verification for scenarios such as:

Applications that are developed by using model-based design, where you perform design verification to demonstrate that the model satisfies the functional requirements and does not contain unintended functionality.
Analyzing a subset of a design model that is intended for control software. For open-loop control analysis, formal verification is widely used for rigorous testing of design models.
Iteratively verifying your model against requirements, checking for design errors, and performing functional testing early in the design cycle and throughout the design process.
Systematic verification and unit-level testing of small components in isolation or for system-level testing of an integrated design model.

When to Use Simulink Design Verifier

Consider a control engineer who is involved in designing a control system. During the design cycle, the control engineer creates a design model from system requirements. Throughout the development process, the engineer:

Identifies and eliminates hidden design errors
Tests model against requirements
Performs model and code coverage analysis to confirm test completeness
Resolves missing coverage by using test generation and dead logic detection
Performs baseline and equivalence testing

Simulink Design Verifier supports these model and code verification processes. It integrates with Requirements Toolbox™, Simulink Coverage™, Simulink Check™, and Simulink Test™ to achieve model and code verification.

Using Simulink Design Verifier in a Model-Based Design Workflow

Model verification includes checking against standards, checking for design errors, proving properties, and generating test cases for coverage analysis.

With Simulink Design Verifier, you can:

Identify hidden design errors, such as integer overflows or division by zero, and generate counterexamples to debug unintended functionalities. You can also justify or exclude model objects from analysis.
Verify model against requirements by using Requirements Toolbox.
Achieve model coverage (Simulink Coverage) by generating test cases that satisfies model coverage objectives.
Perform code coverage (Embedded Coder) analysis by generating test cases for code generated by Embedded Coder^®.
Extend existing test cases and achieve missing coverage.
Integrate test cases with Simulink Test to perform baseline and equivalence testing.
Support industry standards through the IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

This workflow diagram demonstrates the capabilities of Simulink Design Verifier at various stages of the verification and validation workflow.

Workflow diagram of SLDV showng various stages of verification and validation.

For a quick introduction to design error detection and test generation, see Detect Design Errors in Controller Model and Generate Test Cases for a Simplified Cruise Control Model.

To learn more about Simulink Design Verifier analysis, see Detect and Address Bugs, Generate Tests, Prove Properties in a Model, and Review Analysis Results.

Creating Analysis Result Reports

You can also generate reports and review the analysis results. There are several ways to review the analysis results:

Review the analysis results at a glance by highlighting the results on the model.
Create a test harness model to simulate the test cases or debug counterexamples.
Generate a model coverage report.
View generated tests in the Simulation Data Inspector.
Generate an HTML or PDF report that contains detailed information about the analysis results.