使用验证模型证明系统级属性

此示例展示了如何使用验证模型来证明系统级属性。

如果您的模型具有影响模型行为的系统范围的属性，您可能希望在不改变设计模型的情况下证明这些属性。为此，您需要创建一个验证模型，其中包括：

设计模型sldvdemo_sbr_design为安全带提醒灯的逻辑建模。如果打开点火开关，安全带未系好，且车辆超过一定速度，安全带提醒灯就会亮起。

sldvdemo_sbr_verification模型是一个验证模型，它定义了一些约束，并验证了sldvdemo_sbr_design模型中的属性。验证模型中的Model模块引用了设计模型，因此验证逻辑只存在于验证模型中。

由于约束被禁用， sldvdemo_sbr_verification模型包含一个被伪造的属性。在 sldvdemo_sbl_verification_fixed模型中，约束被启用并且所有属性都被证明有效。

请按照以下步骤了解验证模型的工作原理：

1.打开验证模型：

open_system('sldvdemo_sbr_verification')

设计 Model模块是引用 sldvdemo_sbr_design 的 Model模块。设计模型中的 SBR Stateflow ® 图表假设 KEY 输入最初为 0。

2.打开安全属性子系统，指定您想要证明的设计模型的属性。

该子系统包含一个名为MATLAB 属性的MATLAB 功能模块。该模块中的代码指定了当点火开关打开、安全带未系好且速度低于 15 时应开启安全带提醒器的属性：

3.关闭安全属性子系统。

4.打开输入约束子系统。

该子系统定义了以下约束：

5.关闭输入约束子系统，但保持sldvdemo_sbr_verification模型打开。

分析sldvdemo_sbr_verification模型来证明以下属性：

1.在sldvdemo_sbr_verification模型窗口中，要开始分析，双击运行按钮即可开始分析。

当分析完成时，Simulink® Design Verifier[tm] 日志窗口会显示一个目标被证伪——需要仿真。有关更多信息，请参阅目标被证伪——需要仿真。

2.要查看哪个目标被证伪，点击突出显示模型上的分析结果。

安全属性子系统以橙色突出显示。

3.打开安全属性子系统并点击MATLAB属性模块。

Simulink® Design Verifier™ 结果窗口表明语句 sldv.prove(implies(activeCond,SeatBeltIcon)) 在至少一个时间步内为错误。

4.点击查看反例即可查看违反该属性的信号值。

Signal Builder 模块以反例打开。KEY输入最初为2，无效。

要验证安全属性子系统中指定的属性，您必须确保 KEY 的初始值为 0。

验证模型中的输入约束子系统包含三个约束。第三个约束要求KEY的初始值为0，并且KEY只能以1的增量变化，这个约束被禁用。

要查看启用第三个约束时如何验证此属性：

1.在 sldvdemo_sbr_verification模型中，点击打开固定模型。

sldvdemo_sbr_verification_fixed验证模型打开。

2.打开输入约束子系统。

现在启用第三个约束，以便 KEY 的初始值为 0，并且以 1 的增量变化。

3.关闭输入约束子系统。

4.在 sldvdemo_sbr_verification_fixed 模型中，要开始分析，请双击 Run模块。

分析证明了该属性的有效性 .