步骤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。

或者，您可以通过使用模型切片机调试财产侵害。欲了解更多信息，请参阅调试房产证明违反使用型号切片机。

步骤4：打开固定的模式

由计数器例子所表现出的行为errorneous被固定在sldvdemo_cruise_control_verification_fixed模型。

open_system（'sldvdemo_cruise_control_verification_fixed'）;

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

打开参考模型sldvdemo_cruise_control_fixed并打开调节器子系统。在这个子系统中，当主动控制是活性的更新的设计模型复位油门输出。

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

也可以看看