设计和验证模型中的属性

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

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

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

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

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

要执行属性证明分析，点击证明属性。该软件分析模型并在结果摘要窗口中显示结果。结果表明，一个目标在近似下是有效的。

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

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

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