第1步：打开模型

这sldvdemo_cruise_control_verification.模型包含模型引用sldvdemo_cruise_control_defective.设计模型。设计模型是巡航控制系统，该系统由PI控制器组成，该PI控制器基于实际和目标速度之间的差异计算节气门输出。

Open_System（'sldvdemo_cruise_control_verification'）;

节气门输出的安全性能在其中建模安全性质断言块验证子系统。

Open_System（'sldvdemo_cruise_control_verification / safety properties'）;

第2步：执行财产证明分析

在这一点设计验证者选项卡，单击证明属性。

分析完成后，结果摘要窗口报告称一个目标是伪造的。

生成线束模型，并将“信号构建器”对话框打开并显示CounterExample。

步骤3：模拟ConsterExample以复制错误

在“信号构建器”对话框中，单击“开始仿真按钮▸。

诊断查看器窗口显示说明终止模拟的错误，因为发生断言0.04。

可选地，您可以使用模型切片器调试属性冲突。有关更多信息，请参阅使用Model Slicer调试违规的调试属性。

第4步：打开固定模型

柜台示例展出的错误行为是固定的sldvdemo_cruise_control_verification_fixed.模型。

Open_System（'sldvdemo_cruise_control_verification_fixed'）;

在“属性证明工作流程”中，可能需要重新设计系统和/或重新定义属性并执行此类迭代。

打开引用的模型sldvdemo_cruise_control_fixed.并打开控制器子系统。在此子系统中，更新的设计模型在活动控制处于活动状态时重置节气门输出。

在这一点设计验证者选项卡，单击证明属性。分析完成后，结果摘要窗口报告目标有效。

也可以看看