使用 Simulink Design Verifier 证明模型属性

属性是您在 Simulink^® 或 Stateflow^® 中建模或者使用 MATLAB Function 或 Requirements Table 模块建模的需求。属性可以是简单需求，例如模型中的信号在仿真过程中必须达到特定值或值范围。

属性也可以是对模型的需求，涉及将多个输入和输出信号建模为需要被证明的逻辑表达式。

Simulink Design Verifier™ 软件会对您的模型执行形式化分析，以证明指定的属性合规或违规。分析完成后，软件会提供多种结果查看方式：

在模型上突出显示
包含测试用例的框架模型
详细 HTML 报告

用于指定属性证明的证明模块

Simulink Design Verifier 软件提供两个模块，以便您在 Simulink 模型中指定属性证明：

证明模块	描述
Proof Objective	定义要证明的信号的值。
Proof Assumption	在证明过程中约束信号的值。

Simulink 软件中 Model Verification 库中的模块在 Simulink Design Verifier 证明过程中的行为类似于 Proof Objective 模块。您可以使用 Assertion 模块和其他 Model Verification 模块来指定模型的属性。有关这些模块的详细信息，请参阅Model Verification。

用于指定属性证明的证明函数

Simulink Design Verifier 软件提供两个 Stateflow 和 MATLAB^® 代码生成函数，用于指定 Simulink 模型或 Stateflow 图的属性证明：

证明函数	描述
`sldv.prove`	指定证明目标
`sldv.assume`	指定证明假设

这些函数具有以下特点：

识别数学关系，以比使用模块参数更自然的形式证明属性。
支持指定多个目标、假设或条件，而不会使模型复杂化。
提供对 MATLAB 强大功能的访问。
支持验证和模型设计的分离。

有关如何使用这些证明函数的示例，请参阅 sldv.prove 参考页。

注意

Simulink Design Verifier 模块和函数与模型一起保存。如果您在没有 Simulink Design Verifier 许可证的 MATLAB 安装中打开模型，仍可以看到这些模块和函数，但它们不会生成结果。

证明模型属性的工作流

要证明设计模型的属性，请使用以下工作流：

确定设计模型的验证目标，例如，基于您的需求设定进行确定。
对您的设计模型进行插桩以指定证明目标和证明假设。
- 对于简单属性，请使用指定证明目标的模块或 MATLAB 函数对您的模型进行插桩。
- 对于系统级属性，构造一个包含引用设计模型的 Model 模块的验证模型，并使用相同的输入和输出在设计模型接口上定义属性。
使用 Proof Assumption 模块或 sldv.assume 定义分析约束。这些约束适用于所有已启用的证明目标。
注意
证明假设适用于所有已启用的证明目标。请确保您未指定任何相互矛盾的假设，因为这可能会使整个分析无效。
指定控制 Simulink Design Verifier 如何证明模型属性的选项。
执行Simulink Design Verifier 分析并查看结果。

有关演示此工作流的练习，请参阅证明模型中的属性。