Main Content

本页采用了机器翻译。点击此处可查看英文原文。

使用模型切片器调试属性证明违规行为

打开脚本

此示例展示如何使用 Model Slicer 调试属性证明违规。考虑模型sldvdemo_cruise_control_verification 。该模型包含一个断言模块。

验证子系统安全属性模拟了设计模型应具备的属性。该子系统包含一个用于验证属性的断言模块（BrakeAssertion）。Simulink Design Verifier 属性证明分析将尝试证伪该断言。如果 Simulink Design Verifier 成功，它将生成一个反例来证明该断言是错误的。我们可以使用 Model Slicer 来调试这个伪造的断言。

1.打开模型sldvdemo_cruise_control_verification。

open_system ('sldvdemo_cruise_control_verification')

2.通过点击App > Design Verifier打开Simulink Design Verifier。

3.点击证明属性。Simulink Design Verifier 分析模型并在结果摘要窗口中显示结果。

该模型突出显示了Assertion模块所在的子系统。

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

5.单击工具条菜单中的使用切片器调试，以使用模型切片器调试违规行为。或者，您也可以点击结果检查器窗口中的调试。

单击任一入口点，模型上就会完成以下设置：

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

b.该模型通过Simulink Design Verifier分析生成的反例进行突出显示。

c.设计模型在断言失败的时间步处进行仿真并暂停。

6.使用“后退”和“前进”按钮并检查端口标签来调试和分析模型。

  • Assert模块测试 A 的输出是否意味着 B (A==>B) 为false。

  • 当制动输入连续三个时间步为 true 时，A 为 true。

  • 当 Throttle_out <= 0 时，B 为 true

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

a.在Simulation选项卡上，点击Step Back以查看 T = (T-0.1) 时所有模块的端口标签。

你会注意到 A 的端口标签在 T=0.04 之前都是 false，之后变为 true。此时B的端口标签为false（Throttle_Out > 0）。该属性被伪造，因为 Throttle_Out 大于 0 。

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

要查看修复，请打开 sldvdemo_cruise_control_verification模型并点击画布上的打开修复模型按钮。