Simulink Design Verifier
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.
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.
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.
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.
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.