设计和验证模型中的属性

您可以使用 Simulink® Design Verifier™ 将设计需求建模为属性，然后在模型中证明属性。要验证与模型需求关联的属性是否在所有可能的输入值下都成立，请使用属性证明分析。如果需求不成立，Simulink Design Verifier 会提供反例来调试失败情况。

此示例解释如何使用 Proof Objective 模块将设计需求建模为属性，然后在简化的巡航控制模型中验证该属性。

模型 sldvexSimpleCruiseControlProperties 包含验证子系统，该子系统由使用 Proof Objective 模块建模的功能需求组成。

load_system('sldvexSimpleCruiseControlProperty');
open_system('sldvexSimpleCruiseControlProperty/Verification Subsystem');

在 App 选项卡上，点击 App 部分最右侧的箭头。在模型验证、确认和测试库下，点击 Design Verifier。

要执行属性证明分析，请点击证明属性。软件会分析模型，并在“结果摘要”窗口中显示结果。结果指示有一个目标在逼近下有效。

在 Design Verifier 选项卡的“查看结果”部分中，点击在模型中突出显示。

在逼近下有效的属性会以橙色突出显示。点击 Proof Objective 模块。结果检查器窗口会显示 Proof Objective 模块的目标。

要查看 HTML 报告，请在“查看结果”部分中点击 HTML 报告。“证明目标状态”章节会列出在逼近下有效的证明目标。