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