Cruise Control 的财产证明工作流程
此示例显示如何使用 Simulink® Design Verifier™属性证明分析来查找属性违规。您将安全需求模型为属性,然后根据需求验证设计模型。
当您执行属性证明分析时,Simulink Design Verifier 会生成一个反例,您可以使用它来调试属性违规。
步骤 1:打开模型
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');
步骤 2:执行财产证明分析
在Design Verifier选项卡上,点击证明属性。
分析完成后,“结果摘要”窗口将报告一个目标被证伪。
生成框架模型并显示反例。
步骤 3:仿真反例来复制错误
框架模型窗口中,点击全部运行按钮。双击Counterexample_1
模块以打开信号编辑器对话框。单击启动Signal Editor模块图标以打开信号编辑器。
信号编辑器窗口显示一个错误,指出由于在时间 0.04
发生断言,仿真已终止。
您可以选择使用模型切片器来调试属性冲突。有关更多信息,请参阅 使用模型切片器调试属性证明违规行为 。
步骤 4:打开固定模型
反例所表现出的错误行为在sldvdemo_cruise_control_verification_fixed
模型中得到了修复。
open_system('sldvdemo_cruise_control_verification_fixed');
在属性证明工作流程中,您可能需要重新设计系统和/或重新定义属性并执行此类迭代。
打开引用模型sldvdemo_cruise_control_fixed
并打开Controller
子系统。在这个子系统中,更新的设计模型在主动控制处于活动时重置油门输出。
在Design Verifier选项卡上,点击证明属性。分析完成后,“结果摘要”窗口将报告目标有效。