Cruise Control 的财产证明工作流程

此示例显示如何使用 Simulink® Design Verifier™属性证明分析来查找属性违规。您将安全需求模型为属性，然后根据需求验证设计模型。

当您执行属性证明分析时，Simulink Design Verifier 会生成一个反例，您可以使用它来调试属性违规。

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

open_system('sldvdemo_cruise_control_verification');

油门输出的安全属性在Safety Properties验证子系统中由Assertion模块建模。

open_system('sldvdemo_cruise_control_verification/Safety Properties');

在Design Verifier选项卡上，点击证明属性。

分析完成后，“结果摘要”窗口将报告一个目标被证伪。

生成框架模型并显示反例。

框架模型窗口中，点击全部运行按钮。双击Counterexample_1模块以打开信号编辑器对话框。单击启动Signal Editor模块图标以打开信号编辑器。

信号编辑器窗口显示一个错误，指出由于在时间 0.04 发生断言，仿真已终止。

您可以选择使用模型切片器来调试属性冲突。有关更多信息，请参阅使用模型切片器调试属性证明违规行为。

反例所表现出的错误行为在sldvdemo_cruise_control_verification_fixed模型中得到了修复。

open_system('sldvdemo_cruise_control_verification_fixed');

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

打开引用模型sldvdemo_cruise_control_fixed并打开Controller子系统。在这个子系统中，更新的设计模型在主动控制处于活动时重置油门输出。

在Design Verifier选项卡上，点击证明属性。分析完成后，“结果摘要”窗口将报告目标有效。