主要内容

什么是财产证明?

一个财产在Simulink中建模是必须的吗®或Stateflow®，或使用MATLAB函数块。属性可以是一个简单的需求，例如模型中的信号在模拟过程中必须达到一个特定的值或值的范围。

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

的Simulink设计验证器™软件对模型进行形式化分析，以证明或否定指定的属性。在完成分析之后，该软件为您提供了几种检查结果的方法:

  • 在模型上突出显示

  • 一个带有测试用例的控制模型

  • 详细的HTML报告

证明块

的Simulink设计验证器软件提供了两个模块，所以你可以在你的Simulink模型中指定属性证明:

请注意

在Simulink软件中，模型验证库中的块行为类似于证明目标块Simulink设计验证器证明。你可以用断言块和其他模型验证块来指定模型的属性。有关这些块的更多信息，请参见模型验证．

证明函数

的Simulink设计验证器软件提供两个Stateflow和MATLAB®用于代码生成函数指定Simulink模型或状态流图的属性证明:

这些函数:

  • 确定证明属性的数学关系，以一种比使用块参数更自然的形式

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

  • 提供对MATLAB的强大访问。

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

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

请注意

Simulink设计验证器块和函数与模型一起保存。如果您在MATLAB安装中打开模型，那没有Simulink设计验证器许可证，您可以看到块和函数，但它们不会产生结果。

Baidu
map