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