Simulink Design Verifier

Key Features

  • 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.
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.

Formal Methods in Model-Based Design

Simulink Design Verifier uses formal analysis techniques provided by the Prover Plug-In from Prover Technology and the Polyspace formal analysis engine from MathWorks. These techniques rely on mathematically rigorous procedures to search through the possible execution paths of your model for test cases and counterexamples. Unlike traditional testing methods in which test scenarios and expected results are expressed with concrete data values, formal analysis techniques let you work with models of system behavior instead of concrete data values. A model of system behavior can include models of test scenarios and verification objectives that describe desired and undesired system behaviors. Formal analysis performed with such models complements simulation and provides a deeper understanding of your design.

Error Detection Using Formal Methods

Unlike semantic checking or analysis in simulation, formal methods used in Simulink Design Verifier can discover whether specific dynamic execution scenarios can occur and under what conditions. This information can then be used to either improve the design and its requirements or guide the simulation for debugging and validation. Simulink Design Verifier detects the following common design errors: integer overflow, division by zero, dead logic, and assertion violations.

Detecting Integer Overflow and Division by Zero

You use the design error-detection mode in Simulink Design Verifier to discover integer overflow and division by zero. The analysis is automated, and it does not require any additional user input. Permissible ranges for all signals on all blocks are provided to guide you in finding the root cause of the problem. At the end of the analysis, you can review the results directly in the model or in an HTML report.

In the model, blocks are marked as green, yellow, or red. Green blocks have been proven unable to cause integer overflow or division by zero. Yellow blocks occur when the analysis cannot produce a conclusive result or when the time limit for the analysis has been exceeded. When an error is found in the model execution path, all subsequent blocks in that path that can exhibit integer overflow and division by zero are marked yellow.

Red blocks have design errors. For red blocks, Simulink Design Verifier generates a test case that can reproduce the problem during simulation or testing. You can invoke the test case and run a simulation directly within Simulink.

Detecting Dead Logic

You use the test-generation mode in Simulink Design Verifier to detect dead logic, which represents model objects that are either obsolete or are proven to stay inactive during execution. Often dead logic is caused by a design or a requirement error. During code generation, dead logic leads to dead code. Dead logic is difficult to detect by testing in simulation alone because even after running a large number of simulations, it can be difficult to prove that a specific behavior cannot be activated.

At the end of your test-generation analysis, the model is colored according to the test-generation criteria. Model objects containing logic that can’t be activated in simulation are marked red; model objects containing logic that can be fully activated in simulation are marked green. Simulink Design Verifier generates a test case that can reproduce the dead logic during simulation.

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Transition in a Stateflow chart highlighted in red by Simulink Design Verifier. Dead logic occurs for this transition because the condition “press < zero_thresh” can never be false.

Detecting Assertion Violations

You use the violation detection setting of the property-proving mode in Simulink Design Verifier to detect assertion violations. Simulink Design Verifier verifies whether any valid scenarios can trigger assertions during simulation within the number of time steps specified in the analysis settings. For example, you can construct an assertion that triggers whenever a thrust reverser actuator is engaged and a flight-status indicator holds a value of “true.” Assertions that can be violated with valid scenarios are highlighted in red and a test vector that triggers the assertion is generated. In addition to the assertions available in Simulink, Simulink Design Verifier provides additional blocks for defining constraints for the analysis, enabling you to exhaustively analyze design behavior and find design flaws before running a simulation.

Verification of Designs Against Requirements

Functional requirements for discrete systems are typically explicit statements about expected behaviors that a system exhibits and behaviors that it must never exhibit. Behaviors that must never be exhibited are referred to as safety requirements.

Expressing Functional Requirements in Simulink

To formally verify that the design behaves according to these requirements, the requirements statements first need to be translated from a human language into the language understood by the formal analysis engine. Simulink Design Verifier lets you express formal requirements using Simulink, MATLAB® functions, and Stateflow. Each requirement in Simulink has one or more verification objectives associated with it. These verification objectives are used to report whether or not the design meets the functional and safety requirements.

Simulink Design Verifier provides a set of building blocks and functions that you can use to define and organize verification objectives. The block library provided includes blocks and functions for test objectives, proof objectives, assertions, constraints, and a dedicated set of temporal operators for modeling of verification objectives with temporal aspects.

You can group individual requirements and their associated verification objectives into libraries that you can manage and review independently from the design.

Simulink Design Verifier library of property examples.
Simulink Design Verifier library of property examples.

When you use Simulink Design Verifier with the Requirements Management Interface in Simulink Verification and Validation, you can link blocks and functions used to capture requirements and verification objectives to the higher-level textual requirements outside of Simulink.

Proving Designs Against Requirements

Once requirements and verification objectives have been captured in the verification model, they can be used to prove the correctness of a design using formal methods.

To guide the verification of functional requirements and drive your system to a desired state, you can use Test Objective blocks and MATLAB functions for defining test objectives. During test generation Simulink Design Verifier will try to find a valid test case that meets the specified objectives. If an objective can never be satisfied, the design cannot perform the required functionality for a given set of analysis constraints.

To verify the correctness of your design against safety requirements, you can use Proof Objective blocks and MATLAB functions for defining proof objectives. During the analysis Simulink Design Verifier examines all possible input conditions that can cause the undesired behavior and then reports on its findings. For a given proof objective the design can be proven valid, or it can be found to violate safety requirements. When a violation is detected, Simulink Design Verifier generates a test vector that can demonstrate the violation in simulation.

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives. The report shows the list of objectives for which the design was proven valid and the list of objectives for which the analysis found counterexamples.

Validating Analysis Results

Requirements expressed with Simulink, MATLAB functions, and Stateflow can be simulated in parallel with the design. You can also use them to verify generated code cosimulating in SIL mode or PIL mode. The Model Coverage tool accumulates information about activation of verification objectives during simulation and provides coverage results through the Simulink Design Verifier coverage metric. You can speed up root-cause analysis and debugging by using proof objectives that represent safety requirements to stop simulation at the moment of their violation.

Model Coverage Analysis

Simulink Design Verifier analyzes algorithms and logic in your Simulink and Stateflow models to generate test cases and parameters required by industry standards for developing high-integrity systems. Test generation for structural coverage criteria includes condition, decision, and modified condition/decision coverage (MC/DC).

Test Generation

Test generation for model coverage augments requirements-based tests created by hand or collected during simulation of the complete system. With this approach, Simulink Design Verifier takes existing model coverage information and generates additional test vectors that meet all the coverage objectives not satisfied during requirements-based testing.

Requirements-Based Testing
Generate test cases from models of system requirements using Simulink Design Verifier™.

You can use these test vectors to better understand missing requirements and to create a more complete test harness. To simplify testing of models with a large number of inports and outports, Simulink Design Verifier identifies unused signals and automatically removes them from the test harness.

All the generated test vectors are captured as a MATLAB structure that can be used directly as input for the test execution in simulation, SIL, or PIL. The collected test data can also be used to generate a test harness model.

Extend Existing Test Cases to Achieve Full Model Coverage
Leverage existing test cases and achieve full coverage using formal methods for test generation in Simulink Design Verifier™.

Validation of Generated Test Vectors

To validate generated test vectors that meet structural coverage criteria, you can use the Model Coverage tool provided in Simulink Verification and Validation. It monitors simulation and measures whether the objectives reported during formal analysis have been achieved. In addition to coverage objectives for condition, decision, and MC/DC coverage, the Model Coverage tool also reports on the coverage of test objectives, proof objectives, assumptions, constraints, lookup tables, and signal ranges recorded during simulation.

Simulink Design Verifier is certified by TÜV SÜD for use in development processes that must comply with the ISO 26262, IEC 61508, or EN 50128 standards.

Visual display of a generated test vector that activates previously untested functionality.

Visual display of a generated test vector that activates previously untested functionality.

Analysis of Test Coverage on Generated Code

Simulink Design Verifier provides test automation functions for automating the execution of generated test cases against code in SIL and PIL. Code verification functions in Simulink Design Verifier require Embedded Coder. During text execution, you can integrate the code coverage tools available in Embedded Coder for collecting code coverage.

Increasing Robustness of your Software Designs with Simulink

View webinar