什么是财产证明?
属性是您在Simulink®或Stateflow®中模型,或者通过使用MATLAB Function或Requirements Table模块来建模的需求。属性可以是一个简单的需求,例如模型中的信号在仿真期间必须达到特定值或值的范围。
属性也可以是模型上的一个需求,它涉及将多个输入和输出信号建模为需要证明的逻辑表达式。
Simulink Design Verifier™ 软件对您的模型执行正式分析,以证明或反驳指定的属性。完成分析后,软件提供了几种方式供您查看结果:
在模型上突出显示
带有测试用例的框架模型
详细的 HTML 报告
Proof 模块
Simulink Design Verifier 软件提供了两个模块,因此您可以在 Simulink 模型中指定属性证明:
Proof Objective — 定义信号的值来证明
Proof Assumption — 在证明过程中限制信号的值
注意
Simulink 软件中的模型验证库中的模块在 Simulink Design Verifier 证明期间的行为类似于 Proof Objective 模块。您可以使用Assertion模块和其他模型验证模块来指定模型的属性。有关这些模块的更多信息,请参阅 Model Verification 。
证明函数
Simulink Design Verifier 软件提供了两个 Stateflow 和 MATLAB® 用于代码生成函数,以指定 Simulink模型或 Stateflow 图表的属性证明:
sldv.prove
— 指定证明目标sldv.assume
— 指定证明假设
这些函数:
识别数学关系,以比使用模块参数更自然的形式证明属性
支持指定多个目标、假设或条件,而不会使模型复杂化。
提供对 MATLAB 权力的访问权限。
支持验证与模型设计的分离。
有关如何使用这些证明函数的示例,请参阅 sldv.prove
参考页。
注意
Simulink Design Verifier 模块和函数与模型一起保存。如果您在没有 Simulink Design Verifier 许可证的 MATLAB 安装上打开模型,您可以看到模块和函数,但它们不会产生结果。