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

何时使用验证模型进行属性证明

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

关于此示例

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

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

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

了解验证模型

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

1.打开验证模型：

open_system('sldvdemo_sbr_verification')

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

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

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

3.关闭 Safety Properties 子系统。

4.打开 Input Constraints 子系统。

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

5.关闭 Input Constraints 子系统，但保持 sldvdemo_sbr_verification 模型打开。

证明设计模型的性质

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

1.在 sldvdemo_sbr_verification 模型窗口中，要开始分析，点击 Design Verifier 选项卡上的 Prove Properties 以开始分析。

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

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

Safety Properties 子系统以橙色突出显示。

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

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

4.点击查看反例即可查看违反该属性的信号值。sldvdemo_sbr_verification_harness 模型 以 Counterexample_1 作为输入打开。双击 Counterexample_1 打开带有反例的 Signal Editor 模块。点击“打开信号编辑器”按钮 以可视化输入。KEY 输入最初为 2，无效。

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

修复验证模型

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

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

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

sldvdemo_sbr_verification_fixed 验证模型打开。

2.打开 Input Constraints 子系统。

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

3.关闭 Input Constraints 子系统。

4.要开始分析，点击 Design Verifier 选项卡上的证明属性。

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