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。

您可以插入 Proof Objective 模块，而不是使用 sldv.prove 模型。要了解 Proof Objective 模块和 sldv.prove 之间的区别，请参阅使用 Simulink Design Verifier 证明模型属性。

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

在 R2009b 中推出