步骤1:打开模型

的sldvdemo_cruise_control_verification的模型引用sldvdemo_cruise_control_defective设计模型。设计模型是一个巡航控制系统，由PI控制器组成，根据实际速度和目标速度之间的差异计算油门输出。

open_system (“sldvdemo_cruise_control_verification”);

油门输出的安全特性建模在安全属性验证子系统由断言块。

open_system (“sldvdemo_cruise_control_verification /安全属性”);

步骤2:执行属性证明分析

在设计验证器选项卡上,单击证明属性。

分析完成后，结果汇总窗口报告有一个目标被篡改了。

线束模型生成，信号构建器对话框打开并显示反例。

步骤3:模拟反例来复制错误

在“信号生成器”对话框中，单击开始模拟按钮▸。

诊断查看器窗口显示一个错误，说明由于出现断言，模拟已终止0.04。

您可以选择使用模型切片器来调试违反属性的情况。有关更多信息，请参见调试属性证明违反使用模型切片器。

第四步:打开固定模型

反例所显示的错误行为是固定的sldvdemo_cruise_control_verification_fixed模型。

open_system (“sldvdemo_cruise_control_verification_fixed”);

在属性证明工作流中，您可能需要重新设计系统和/或重新定义属性并执行这样的迭代。

打开被引用的模型sldvdemo_cruise_control_fixed并打开控制器子系统。在这个子系统中，更新的设计模型重置节流输出时，主动控制是主动的。

在设计验证器选项卡上,单击证明属性。分析完成后，结果摘要窗口报告目标是有效的。

另请参阅