Main Content

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

证明模型属性的工作流程

为了证明设计模型的属性，请使用以下工作流程：

  1. 确定您的设计模型的验证目标，例如根据您的需求规范。

  2. 使用您的设计模型来指定证明目标和证明假设。

    • 对于简单属性，使用指定证明目标的模块或MATLAB®函数来装备你的模型。

    • 对于系统级属性，构建一个包含引用设计模型的Model模块的验证模型，并使用相同的输入和输出在设计模型接口上定义属性。

  3. 使用 Proof Assumption模块或 sldv.assume 定义分析约束。这些约束适用于所有启用的证明目标。

    注意

    证明假设适用于所有启用的证明目标。确保没有指定任何矛盾的假设，因为这可能会使整个分析无效。

  4. 指定控制 Simulink® Design Verifier™ 如何证明模型属性的选项。

  5. 执行Simulink Design Verifier分析并查看结果。

有关演示此工作流程的练习，请参阅 证明模型中的属性 。

相关主题