验证子系统安全属性建模一个应该适用于设计模型的属性。这个子系统包含一个断言块(BrakeAssertion)来验证属性。证明分析将尝试对断言进行证伪。如果Simulink Design Verifier是成功的，它将生成一个反例来证伪断言。我们可以使用Model Slicer来调试这个伪断言。

1.开放模式sldvdemo_cruise_control_verification．

open_system (“sldvdemo_cruise_control_verification”）

2.点击打开Simulink设计验证器应用程序>设计验证器．

3.点击证明属性．Simulink Design Verifier对模型进行分析，并在“结果汇总”窗口中显示结果。

该模型突出了子系统断言块的位置。

4.打开安全属性子系统并选择已伪造的断言块。

5.点击调试使用切片机从工具条菜单中使用Model Slicer来调试违规。您也可以单击调试在结果检查器窗口中。

单击任意一个入口点，在模型上完成以下设置:

a.添加断言块作为模型切片器的起点。

b.用Simulink Design Verifier分析生成的反例突出显示模型。

c.模拟设计模型，在断言失败的时间步处暂停。

6.通过使用“后退”和“前进”按钮调试和分析模型，并检查Port标签。

您可以注意到，当条件A==>B为假时，模拟在t=0.04处停止。这可以从端口标签中观察到。

一。模拟选项卡上,单击退一步查看T = (T-0.1)处所有块的端口标签。

您可以注意到的Port标签一个是假直到T=0.04，当它变成真正的．的Port标签B是假(Throttle_Out >)Throttle_Out大于0．

b.查看导致失败的块设计模型>控制器．相关的块和路径被突出显示。

要查看修复，请打开sldvdemo_cruise_control_verification模型和点击开放的固定模式按钮在画布上。