财产证明用于巡航控制的工作流程

开放示例

此示例显示了如何通过使用Simulink®Designverifier™属性证明分析来查找违规行为。金宝app您将安全要求将其建模为属性，然后根据要求验证设计模型。

当您执行属性证明分析时，Simulink Design验证者会生成用于调试属性违规的反例金宝app。

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

open_system（'sldvdemo_cruise_control_verification'）；

油门输出的安全性能在安全性能通过断言块验证子系统。

open_system（'sldvdemo_cruise_control_verification/Safety Properties'）；

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

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

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

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

诊断查看器窗口显示出一个错误，指出模拟终止，因为在时间上发生断言0.04。

可选地，您可以使用模型切片机调试违规属性。有关更多信息，请参阅调试财产通过使用模型切片机证明违规行为。

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

open_system（'sldvdemo_cruise_control_verification_fixed'）；

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

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

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