步骤1:打开模型

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

open_system (“sldvdemo_cruise_control_verification”)；

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

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

步骤2:进行性质证明分析

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

在分析完成后，Results Summary窗口报告有一个目标被伪造。

脊甲模型生成，Signal Builder对话框打开并显示反例。

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

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

“诊断查看器”窗口显示一个错误，说明由于当时发生断言，模拟已终止０．０４．

您还可以选择使用Model Slicer调试属性冲突。有关更多信息，请参见调试属性使用模型切片器证明违规．

步骤4:打开固定模型

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

open_system (“sldvdemo_cruise_control_verification_fixed”)；

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

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

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

另请参阅