Property Proving Workflow for Cruise Control
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.
When you perform property proving analysis, Simulink Design Verifier generates a counterexample that you use to debug the property violation.
Step 1: Open the Model
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.
The safety properties for the throttle output are modeled in the
Safety Properties verification subsystem by the Assertion block.
Step 2: 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 is generated and the Signal Builder dialog box opens and displays the counterexample.
Step 3: Simulate the Counterexample to Replicate the Error
In the Signal Builder dialog box, click the Start simulation button ▸ .
The Diagnostic Viewer window displays an error stating that the simulation was terminated because an assertion occurred at time
Optionally, you can debug the property violation by using the Model Slicer. For more information, see Debug Property Proving Violations by Using Model Slicer.
Step 4: Open the Fixed Model
The erroneous behavior exhibited by the counter example is fixed in the
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.