指定并验证设计需求
安全需求定义模型中的意外行为。Simulink® Design Verifier™ 使用属性证明来验证与模型需求相关联的属性在所有可能的输入值下是否成立，或者提供导致违规的反例。您可以使用 Simulink Design Verifier 将设计需求建模为属性，然后证明模型中的属性。
模块
函数
主题
- 使用 Simulink Design Verifier 证明模型属性
属性证明概述。
- 证明模型中的属性
提供一个示例，引导您完成证明模型属性的过程。
- 使用模型切片器调试属性证明违规行为
使用模型切片器通过断言模块调试您的设计。
- 使用验证模型证明系统级属性
使用验证模型来证明系统级属性的示例。
- 使用 Proof Objective 模块进行属性证明
您可以使用 Simulink® Design Verifier™ 将设计需求建模为属性，然后在模型中证明属性。要验证与模型需求关联的属性是否在所有可能的输入值下都成立，请使用属性证明分析。如果需求不成立，Simulink Design Verifier 会提供反例来调试失败情况。
- 使用 MATLAB Function 模块进行属性证明
此示例说明如何验证安全带提醒装置设计模型。该模型下方的 Safety Properties 模块包含在 MATLAB® 中指定的一个属性，该属性指示图标何时应处于活动状态。Simulink® Design Verifier™ 会分析设计模型和安全属性，以证明正确性或识别反例。在此模型中，由于设计隐式假设 KEY 输入从 0 开始并以 1 为增量变化，因此违反了该属性。
- 使用 MATLAB Truth Table 模块进行属性证明
此示例说明如何验证上方顶层模块中引用的安全带提醒装置设计模型。该模型下方的 Safety Properties 模块包含在 MATLAB Truth Table 中指定的一个属性，该属性指示 SeatBeltIcon 输出何时应处于活动状态。Simulink® Design Verifier™ 会分析设计模型和安全属性，以证明正确性或识别反例。在此模型中，该属性的证明基于以下显式假设：KEY 输入从 0 开始并以 1 为增量变化。
- 使用 Assumption 模块进行属性证明
此示例说明如何使用 Proof Assumption 模块执行 Simulink® Design Verifier™ 属性证明。它尝试证明，在当前输入值与之前的六个输入值之和大于 6 时，输出等于 2。该模型包含一个 Proof Assumption 模块，该模块将输入限制为 0 或 1。Simulink Design Verifier 搜索 20 个或更少的时间步内是否存在违规。由于该属性在假设下有效，因此无法找到违规。
- 包含无效属性的属性证明
此示例说明如何使用 Simulink® Design Verifier™ 属性证明分析找出无效属性。它尝试证明，在当前输入值与之前的六个输入值之和大于 6 时，输出等于 2。在本例中，由于单个较大的输入值（例如 255）导致总和大于 6，因此该属性是无效的。Simulink Design Verifier 会生成一个反例来演示违规。
- 去抖时序属性
对属性证明和测试用例生成的时序系统需求进行建模。
- 电动车窗控制器时间属性
此示例展示了如何使用 Simulink® Design Verifier™ Temporal Operator 模块在电动车窗控制器模型中对时间系统需求模型，以进行属性证明和测试用例生成。
- 证明大型模型中的属性
描述证明大型模型中的属性的工作流程和最佳实践。
- 验证并确认模型和代码
定义需求、测试模型和代码，检查设计错误和标准合规性，并测量测试覆盖率。
- 使用观察者隔离验证逻辑
使用 Observer 模块将验证逻辑隔离在模型中。
精选示例
通过分析模型属性来验证需求
分析控制系统模型是否符合以属性建模的需求，并使用依存关系性分析调查属性违规行为。
使用 Simulink Design Verifier 查找和调试属性违规
使用 Simulink Design Verifier 查找和调试模型中的属性违规。
反推装置的属性证明工作流
此示例说明如何在反推装置设计模型中验证安全属性。该模型下方的 Properties 模块包含四个安全属性。Simulink® Design Verifier™ 会分析设计模型和安全属性，以证明正确性或识别反例。使用模型引用无需在设计模型中添加验证内容，使得验证内容可以独立于设计而存在。
使用多个属性进行属性证明
此示例说明如何使用多个属性执行属性证明分析。该模型配置为进行分析以尝试证明：
带模块替换的定点巡航控制的属性证明工作流程
此示例说明如何证明定点巡航控制算法中的属性。它通过模型引用来引用设计模型，使得原有的设计模型保持不变。模块替换规则指定检查是否可能发生溢出的属性。验证子系统指定了属性证明时对速度输入范围的假设。该模型配置 Simulink Design Verifier 以将模块替换应用于 Sum 模块，该模块为引用模型中的定点 PI 控制器的输出端口提供数据，并返回演示溢出的反例。
使用 Observer Reference 模块进行属性证明分析
使用 Observer Reference 模块执行属性证明分析。
使用 Requirements Table 模块证明属性
使用 Requirements Table 模块和 Simulink Design Verifier 来证明模型的属性。
