Get Started with Simulink Design Verifier

Identify design errors, prove requirements compliance, and generate tests

Simulink^® Design Verifier™ uses formal methods to identify hidden design errors in models. It detects blocks in the model that result in integer overflow, dead logic, array access violations, and division by zero. It can formally verify that the design meets functional requirements. For each design error or requirements violation, it generates a simulation test case for debugging.

Simulink Design Verifier generates test cases for model coverage and custom objectives to extend existing requirements-based test cases. These test cases drive your model to satisfy condition, decision, modified condition/decision (MCDC), and custom coverage objectives. In addition to coverage objectives, you can specify custom test objectives to automatically generate requirements-based test cases.

Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

Acknowledgments

Tutorials

About Systematic Model Verification Using Simulink Design Verifier

Overview of features and capabilities of Simulink Design Verifier to help you get started with formal verification.
Overview of the Simulink Design Verifier Workflow

Overview of the basic Simulink Design Verifier workflow.
Detect Design Errors in Controller Model

Identify hidden design errors in your model by using design error detection analysis.
Generate Test Cases for a Simplified Cruise Control Model

Analyze a simple control system model that demonstrates Simulink Design Verifier capabilities.

Featured Examples

Detect Integer Overflow Errors

Detect integer overflow errors in a model by using design error detection analysis. Simulink® Design Verifier™ identifies the model constructs that may result in integer overflows and then either proves that the integer overflow cannot occur during simulation or generates test cases that demonstrates the integer overflow error.

Open Script

Property Proving Workflow for Cruise Control

Find a property violation by using Simulink® Design Verifier™ property proving analysis. You model safety requirements as properties and then verify the design model against requirements.

Open Script

Cruise Control Test Generation

Generate test cases that achieve complete model coverage. By default, Simulink® Design Verifier™ generates test cases that satisfy objectives in the fewest steps. One of the test objectives forces the discrete integrator in the PI controller to exceed its upper limit. When you run Simulink Design Verifier without constraints, the limit is exceeded in a single step by forcing speed to be 500. The constraint on speed limits the values in test cases between 0 and 100. This forces the test cases to take several samples to exceed the integrator limit.

Open Script

Videos

What Is Simulink Design Verifier?
Introduction to Simulink Design Verifier.

Requirements and Advanced Model Checks Workflow
Manage requirements in Simulink, perform advanced model checks, and check your model for run-time errors.

Requirements-Based Testing Workflow
Explains how to create a test using a test sequence, define a formal assessment, link test cases to requirements, run test suites, and analyze missing model test coverage.