Simulink Design Verifier

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.

Next: Model Coverage Analysis

Try Simulink Design Verifier

Get trial software

Simulink Products for HVAC Controls Software

Watch video