Step 1: Open the Model

Thesldvdemo_cruise_control_verificationmodel contains a model reference to thesldvdemo_cruise_control_defectivedesign 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 theSafety Propertiesverification subsystem by the Assertion block.

open_system('sldvdemo_cruise_control_verification/Safety Properties');

Step 2: Perform Property Proving Analysis

On theDesign Verifiertab, clickProve 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 theStart simulationbutton ▸ .

The Diagnostic Viewer window displays an error stating that the simulation was terminated because an assertion occurred at time0.04.

Optionally, you can debug the property violation by using the Model Slicer. For more information, seeDebug Property Proving Violations by Using Model Slicer.

Step 4: Open the Fixed Model

The erroneous behavior exhibited by the counter example is fixed in thesldvdemo_cruise_control_verification_fixedmodel.

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 modelsldvdemo_cruise_control_fixedand open theControllersubsystem. In this subsystem, the updated design model resets the throttle output when Active Control is active.

On theDesign Verifiertab, clickProve Properties. After the analysis completes, the Results Summary window reports that the objective is valid.

See Also