Debug Property Proving Violations by Using Model Slicer

Open Script

This example shows how to debug property proving violations by using Model Slicer. Consider the model sldvdemo_cruise_control_verification. This model contains an Assertion block.

The Verification subsystem Safety Properties models a property that should hold true for the design model. This subsystem contains an Assertion Block (BrakeAssertion) that verifies the property. Simulink Design Verifier Property Proving analysis will try to falsify the assertion. If Simulink Design Verifier is successful it will generate a counterexample falsifying the assertion. We can use Model Slicer to debug this falsified assertion.

1. Open model sldvdemo_cruise_control_verification.

open_system ('sldvdemo_cruise_control_verification')

2. Open Simulink Design Verifier by clicking on Apps > Design Verifier.

3. Click Prove Properties. Simulink Design Verifier analyses the model and displays the results in Results Summary window.

The model highlights the subsystem where the Assertion block is located.

4. Open Safety Properties subsystem and select the falsified Assertion block.

5. Click Debug Using Slicer from the toolstrip menu to debug the violation using Model Slicer. Alternatively, you can click Debug in the results Inspector window.

On Clicking either of the entry points the following setup is done on the model:

a. The Assertion block is added as a starting point for Model Slicer.

b. The model is highlighted with the counterexample generated by Simulink Design Verifier analysis.

c. The design model is simulated and paused at the time-step of assertion failure.

6. Debug and analyze the model by using the Step Back and Step Forward buttons, and inspecting the Port labels.

The Assert block tests if the output of A implies B (A==>B) is false.
A is true when the brake input in is true for three consecutive time steps.
B is true when the Throttle_out <= 0

You can notice that the simulation is stopped at t=0.04 when the condition A==>B is false. This can be observed from the Port labels.

a. On the Simulation tab, click the Step Back to see the port labels of all the blocks at T = (T-0.1).

You can notice that the Port label of A is false till T=0.04, when it becomes true. At this point the Port label of B is false (Throttle_Out > 0). The property is falsified because Throttle_Out is greater than 0.

b. To view the blocks that results in the failure, open the Design Model > Controller. The dependent blocks and path are highlighted.

To view the fix, open sldvdemo_cruise_control_verification model and the click the Open Fixed Model button on the canvas.