sldv.prove

用于 Stateflow 图和 MATLAB Function 模块的证明目标函数

语法

sldv.prove(expr)

sldv.prove(expr) 指定在证明属性时，expr 在每次计算时都为 true。可以对 expr 使用任何有效的布尔表达式。

此函数没有输出，也不会对其父函数产生任何影响，但会对计算 expr 产生间接副作用。如果从 MATLAB^® 命令行发出该函数，则该函数无效。

可以在代码中穿插使用 sldv.prove 证明假设，也可以将假设单独放在验证脚本中。

使用 MATLAB Function 模块在 sldvdemo_sbr_verification 模型中指定属性证明目标和证明假设。

下面的命令会打开一个关联了 sldvdemo_sbr_verification 模型的示例。打开模型。

openExample('sldv/SldvexCCallerBlockExample')

将 sldvdemo_sbr_verification 另存为 ex_sldvdemo_sbr_verification。

打开 Safety Properties 子系统。

打开 MATLAB Property 模块，它是一个 MATLAB Function 模块。

在 check_reminder 函数定义的末尾添加 sldv.assume(Inputs.KEY==0 | 1);，这样函数定义的最后两行为：

sldv.prove(implies(activeCond, SeatBeltIcon));
sldv.assume(Inputs.KEY==0 | 1);

保存模型并返回到顶层模型。

要证明安全属性，请在 Simulink^® 编辑器中选择 Safety Properties 子系统。在 Design Verifier 选项卡上点击证明属性。

或者，在 Simulink 编辑器中，您可以右键点击 Safety Properties 子系统，然后依次选择 Design Verifier > 证明子系统属性。

假设表达式，指定为布尔表达式。例如，x > 0。

除了使用 sldv.prove 函数外，您还可以在模型中插入 Proof Objective 模块。要了解 Proof Objective 模块与 sldv.prove 之间的区别，请参阅使用 Simulink Design Verifier 证明模型属性。

您也可以通过使用 MATLAB 生成代码来指定证明目标，而无需使用 sldv.prove 函数。使用 sldv.prove 而不是直接使用 MATLAB 生成代码可以省去以下操作：

在 R2009b 中推出