使用验证模型证明系统级属性
此示例展示了如何使用验证模型来证明系统级属性。
何时使用验证模型进行财产证明
如果您的模型具有影响模型行为的系统范围的属性,您可能希望在不改变设计模型的情况下证明这些属性。为此,您需要创建一个验证模型,其中包括:
引用设计模型的Model模块
定义属性和任何所需约束的一个或多个验证子系统
关于此示例
设计模型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.打开输入约束子系统。
该子系统定义了以下约束:
该键可以处于三个位置:0、1、2
速度被限制在 10 到 30 之间。
密钥必须从 0 开始,并且每次只能改变一个增量。例如,密钥可以从 0 变为 1 或从 1 变为 2,但不能从 0 变为 2。在本验证模型中,该约束未启用。
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模块。
分析 证明 了 该属性的 有效性 .