Find and Debug Property Violation Using Simulink Design Verifier
Simulink® Design Verifier™ uses property proving to confirm that the properties linked to model requirements hold across all potential input values or identifies counterexamples that result in violations. For more information on property proving analysis, see Specify and Verify Design Requirements.
This example shows how to find a property violation by using Simulink® Design Verifier™ property proving analysis. You model safety requirements as properties and then verify the design model against requirements. Then, you perform property proving analysis where Simulink Design Verifier generates a counterexample that you use to debug the property violation. For more information, see Prove Model Properties Using Simulink Design Verifier
Open the Model
The sldvdemo_cruise_control_verification model contains a model reference to the sldvdemo_cruise_control_defective design model. The design model is a cruise control system that consists of a PI Controller that computes the throttle output based on the difference between the actual and target speed.
open_system('sldvdemo_cruise_control_verification');
The safety properties for the throttle output are modeled in the Safety Properties verification subsystem by the Assertion block.
open_system('sldvdemo_cruise_control_verification/Safety Properties');
The throttle goes to zero when the brake is applied for three consecutive steps.
Perform Property Proving Analysis
On the Design Verifier tab, click Prove Properties. After the analysis completes, the Results Summary window reports that one objective was falsified.
The harness model sldvdemo_cruise_control_verification is generated and displays the counterexample. For more information, see Proof Objectives Status.
Simulate Counterexample to Replicate Error
In the harness model window, click the Run All button. Double-click on Counterexample_1 block to open the Block Parameters dialog box. Click on Launch Signal Editor block icon to observe the simulation. For more information on harness model, see Manage Simulink Design Verifier Harness Models.
The Signal Editor window displays an error stating that the simulation was terminated because an assertion occurred at time 0.04.
Optionally, you can debug the property violation by using the Model Slicer. For more information, see Debug Property Proving Violations by Using Model Slicer.
Perform Analysis on Fixed Model
The erroneous behavior exhibited by the counterexample is fixed in the sldvdemo_cruise_control_verification_fixed model.
open_system('sldvdemo_cruise_control_verification_fixed');
In the property proving workflow, you may be required to redesign the system and/or redefine the property and perform such iterations.
Open the referenced model sldvdemo_cruise_control_fixed and open the Controller subsystem. In this subsystem, the updated design model resets the throttle output when Active Control is active.
On the Design Verifier tab, click Prove Properties. After the analysis completes, the Results Summary window reports that the objective is valid.
