Main Content

本页采用了机器翻译。点击此处可查看英文原文。

什么是财产证明？

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

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

Simulink Design Verifier™ 软件对您的模型执行正式分析，以证明或反驳指定的属性。完成分析后，软件提供了几种方式供您查看结果：

  • 在模型上突出显示

  • 带有测试用例的框架模型

  • 详细的 HTML 报告

Proof 模块

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

注意

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

证明函数

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

这些函数：

  • 识别数学关系，以比使用模块参数更自然的形式证明属性

  • 支持指定多个目标、假设或条件，而不会使模型复杂化。

  • 提供对 MATLAB 权力的访问权限。

  • 支持验证与模型设计的分离。

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

注意

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