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