sldv.prove

Stateflow 图表和 MATLAB 函数模块的证明目标函数

语法

sldv.prove(expr)

sldv.prove(expr) 指定在证明属性时，expr 对于每次评估都为真。对 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 之间的区别，请参阅什么是财产证明？。

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

在 R2009b 中推出