使用 Simulink Design Verifier 查找和调试属性违规
Simulink® Design Verifier™ 使用属性验证来确认与模型需求相关的属性在所有潜在输入值下均成立，或识别导致违规的反例。有关属性证明分析的更多信息，请参阅 指定并验证设计需求。
此示例显示如何使用 Simulink® Design Verifier™ 属性证明分析来查找属性违规。您将安全需求模型为属性，然后根据需求验证设计模型。然后，执行属性证明分析，其中 Simulink Design Verifier 生成一个反例，用于调试属性违规。有关详细信息，请参阅使用 Simulink Design Verifier 证明模型属性
打开模型
sldvdemo_cruise_control_verification 模型包含对 sldvdemo_cruise_control_defective 设计模型的模型引用。设计模型是一个巡航控制系统，由一个 PI 控制器组成，该控制器根据实际速度和目标速度之间的差异计算油门输出。
open_system('sldvdemo_cruise_control_verification');
油门输出的安全属性在 Safety Properties 验证子系统中由 Assertion 模块建模。
open_system('sldvdemo_cruise_control_verification/Safety Properties');
当制动器连续踩下三次时，节气门会完全关闭。
执行属性证明分析
在 Design Verifier 选项卡上，点击证明属性。分析完成后，“结果摘要”窗口将报告一个目标被证伪。
生成了框架模型 sldvdemo_cruise_control_verification，并显示了反例。有关详细信息，请参阅证明目标状态。
仿真反例以复制错误
在框架模型窗口中，点击全部运行按钮。双击 Counterexample_1 模块，打开“模块参数”对话框。点击“启动 Signal Editor”模块图标，观察仿真。有关框架模型的更多信息，请参阅管理 Simulink Design Verifier 框架模型。
信号编辑器窗口显示一个错误，指出由于在时间 0.04 发生断言，仿真已终止。
您可以选择使用模型切片器来调试属性冲突。有关详细信息，请参阅 使用模型切片器调试属性证明违规行为。
对固定模型进行分析
反例所表现出的错误行为在 sldvdemo_cruise_control_verification_fixed 模型中得到了修复。
open_system('sldvdemo_cruise_control_verification_fixed');
在属性证明工作流程中，您可能需要重新设计系统和/或重新定义属性并执行此类迭代。
打开引用模型 sldvdemo_cruise_control_fixed 并打开 Controller 子系统。在这个子系统中，更新的设计模型在主动控制处于活动时重置油门输出。
在 Design Verifier 选项卡上，点击证明属性。分析完成后，“结果摘要”窗口将报告目标有效。
