Key Features

  • Test case input generation from functional requirements and model coverage objectives, including condition, decision, and MCDC
  • Detection of dead logic, integer and fixed-point overflows, array access violations, division by zero, and violations of design requirements
  • Verification blocks for modeling functional and safety requirements
  • Property proving, with generation of violation examples for analysis and debugging
  • Model Slicer for analyzing functional dependencies and problematic behavior in large models
  • Variant Reducer for creating sliced models based on active variant configurations
  • Polyspace® and Prover® formal verification engines for fixed-point and floating-point models
Identify design errors, generate test cases, and verify designs against requirements using Simulink Design Verifier.

Simulink Design Verifier™ lets you verify your designs and validate requirements early without having to generate code. It helps you increase robustness of your designs within the Simulink® environment. You can analyze control logic, S-functions, and MATLAB® code using mathematically rigorous formal methods. Unlike traditional testing methods in which test scenarios and expected results are expressed with concrete data values, formal verification techniques let you work with models of system behavior instead. Formal verification can prove certain attributes of software, such as whether software contains run-time errors or not, providing deeper understanding of the system’s requirements.

Design Error Detection

Simulink Design Verifier can discover whether specific dynamic execution scenarios can occur and under what conditions. You can detect the following design errors: integer overflow, division by zero, dead logic, and array out of bounds. Finding these errors early in the design cycle, before simulation-based testing, prevents costly fixes later on.

Design error detection is completely automated, and you can review the results directly in the model or in an HTML report. Permissible ranges for all signals on all blocks are provided to guide you in finding the root cause of the problem. In the model, blocks are marked as green, orange, or red: green indicates no error detected, orange indicates the analysis was inconclusive in the time provided, and red indicates blocks that exhibit design errors. Simulink Design Verifier automatically generates test case inputs to recreate the error scenario for each red block. You can use these test inputs in Simulink to understand and debug the conditions under which the error occurs.

Design error detection. Block highlighted in red has a design error; the subsystem highlighted in green is proven correct.

Dead Logic Detection

Dead logic detection mode finds objects in the model that are either obsolete or are found 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. Model objects containing logic that cannot be activated in simulation are marked red; model objects containing logic that can be fully activated in simulation are marked green. 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.

Dead logic detection, with 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.

Test Case Input Generation

Verifying the input-output behavior of the implementation model alone does not guarantee design correctness. Functional tests are a great first step for model verification, but these tests are essentially derived from requirements, which might be incomplete. To increase robustness of your design, you can use structural verification techniques such as model coverage to help identify unused simulation pathways in the model. In essence, model coverage is a measure of how thoroughly a test case exercises a model and tells you the percentage of pathways that a test case exercises. By investigating untested pathways, you can detect potential design errors.

Leverage existing test cases and achieve full coverage using formal methods for test generation in Simulink Design Verifier.

Simulink Design Verifier combines formal methods and heuristic techniques to generate test cases for model coverage and custom user criteria. Test case generation for model coverage augments and extends requirements-based test inputs created by hand or collected during simulation of the complete system. In addition to coverage objectives for condition, decision, and MCDC coverage, you can also specify custom test objectives to generate requirements-based test cases.

Generate test cases from models of system requirements using Simulink Design Verifier.

You can use the Test Generation Advisor to select model components (atomic subsystems and model blocks) for test generation. The Generation Advisor performs a high-level analysis to help you better understand your model before test generation, particularly for large models, complex models, or models for which you are uncertain of the test generation compatibility. All the generated test case inputs are captured as a MATLAB structure that can be used directly as an input for test execution in simulation, SIL, or PIL. The collected test data can also be used with Simulink Test™ and associated test harnesses. During test execution, you can integrate with third-party code coverage tools available in Embedded Coder® for collecting code coverage.

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.

Test Generation Advisor: Summary of test generation compatibility, coverage objectives, and dead logic for the model and model components in hierarchical view.

Isolating Problematic Behavior with Model Slicer

Simulink Design Verifier isolates behaviors of interest in a model using a combination of dynamic and static analysis to trace dependencies. Dependency analysis includes determining dependencies of blocks, signals, and model components. This is a lengthy process for large models given the levels of hierarchy and design complexity. Model Slicer helps you understand which parts of your model impact a particular behavior. Using static analysis, you can identify model dependencies for all possible simulation paths; whereas, using simulation-based analysis highlights only paths active during simulation.

Debug complex designs faster by highlighting functional dependencies and producing a simplified model with the Model Slicer feature in Simulink Design Verifier.

The dependency analysis propagates upstream, downstream, or bidirectionally from a starting point. You can highlight and trace functional dependencies of ports, signals, and blocks, and slice a large model into smaller, standalone models for analysis. You can also view blocks affecting a subsystem output and trace a signal path through multiple switches and logic blocks.

Test and debug complex models. Identify the area of interest in your model and generate a sliced model for further analysis and debugging.

Simplify Variant Systems with Variant Reducer

You can use Variant Reducer to create a simplified, standalone model containing only the active variant configuration. When you highlight functional dependencies in a model containing variant systems, only active variant choices are highlighted. When you create a simplified standalone model from a model highlight that includes variant systems, Variant Reducer removes the variant systems and replaces them with the active variant configurations.

Requirements-Based Verification

To formally verify that a design behaves according to certain functional or safety 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 MATLAB functions, Simulink, and Stateflow®. Each requirement in Simulink has one or more verification objectives associated with it. Once requirements and verification objectives have been captured, they can be used to prove the correctness of a design using formal methods.

For example, in a flight tracking system, you might construct an assertion or proof objective that triggers whenever a thrust reverser actuator is engaged and a flight-status indicator holds the value of “true.” 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 a safety requirement. When it detects a violation, Simulink Design Verifier generates a test case that can demonstrate the violation in simulation.

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

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.