指定并验证设计需求
根据需求验证设计，使用输入假设优化反例
安全需求定义模型中的意外行为。Simulink® Design Verifier™ 使用属性证明来验证与模型需求相关联的属性在所有可能的输入值下是否成立，或者提供导致违规的反例。您可以使用 Simulink Design Verifier 将设计需求建模为属性，然后证明模型中的属性。
模块
函数
主题
入门知识
- 证明模型属性的工作流
- 使用 Simulink Design Verifier 证明模型属性
属性证明概述。 - 证明模型中的属性
提供一个示例，引导您完成证明模型属性的过程。 - 使用参数表查找约束
如何将参数指定为分析的变量的示例。 - 指定信号范围
指定信号在仿真期间可以达到的最小值和最大值。通过指定信号在仿真过程中可以达到的最小值和最大值，充分指定您的设计并优化数据类型和生成的代码。 - 最小和最大输入约束
Simulink Design Verifier 分析如何考虑指定的输入最小值和最大值的概述。 - 指定 Simulink 和 Stateflow 元素的输入范围
描述分析如何处理 Simulink 和 Stateflow® 元素的最小值和最大值。 - 验证并确认模型和代码
定义需求、测试模型和代码，检查设计错误和标准合规性，并测量测试覆盖率。
用于验证和确认的需求建模
- 指定 Simulink 和 Stateflow 元素的输入范围
描述分析如何处理 Simulink 和 Stateflow 元素的最小值和最大值。 - 使用规范模型进行基于需求的测试
按照系统的方法根据需求验证您的设计模型。 (自 R2022b 起)
通过属性证明进行验证
- 证明模型中的属性
提供一个示例，引导您完成证明模型属性的过程。 - 设计和验证模型中的属性
您可以使用 Simulink® Design Verifier™ 将设计需求建模为属性，然后在模型中证明属性。要验证与模型需求关联的属性是否在所有可能的输入值下都成立，请使用属性证明分析。如果需求不成立，Simulink Design Verifier 会提供反例来调试失败情况。 - 使用模型切片器调试属性证明违规行为
使用模型切片器通过断言模块调试您的设计。 - 使用验证模型证明系统级属性
使用验证模型来证明系统级属性的示例。 - 证明子系统中的属性
解释如何证明子系统中的属性。 - 检查指定的最小值和最大值违规
描述如何分析模型以验证是否遵守指定的设计最小值和最大值。 - sldvData 字段中输入范围的规范
描述最小和最大输入值的sldvData字段。 - 使用 MATLAB Function 模块进行属性证明
此示例说明如何验证安全带提醒装置设计模型。该模型下方的 Safety Properties 模块包含在 MATLAB® 中指定的一个属性，该属性指示图标何时应处于活动状态。Simulink® Design Verifier™ 会分析设计模型和安全属性，以证明正确性或识别反例。在此模型中，由于设计隐式假设 KEY 输入从 0 开始并以 1 为增量变化，因此违反了该属性。 - 使用 MATLAB Truth Table 模块进行属性证明
此示例显示如何验证上面顶部模块中引用的安全带提醒设计模型。其下方的安全属性模块包含 MATLAB 真值表中指定的属性，该属性指示 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 给出了一个反例来证明违规行为。 - 证明大型模型中的属性
描述证明大型模型中的属性的工作流程和最佳实践。
精选示例
通过分析模型属性来验证需求
分析控制系统模型是否符合以属性建模的需求，并使用依存关系性分析调查属性违规行为。
Cruise Control 的属性证明工作流程
此示例显示如何使用 Simulink® Design Verifier™ 属性证明分析来查找属性违规。您将安全需求模型为属性，然后根据需求验证设计模型。
反推装置的属性证明工作流
此示例说明如何在反推装置设计模型中验证安全属性。该模型下方的 Properties 模块包含四个安全属性。Simulink® Design Verifier™ 会分析设计模型和安全属性，以证明正确性或识别反例。使用模型引用无需在设计模型中添加验证内容，使得验证内容可以独立于设计而存在。
使用多个属性进行属性证明
此示例说明如何使用多个属性执行属性证明分析。该模型配置为进行分析以尝试证明：
带模块替换的定点巡航控制的属性证明工作流程
此示例说明如何证明定点巡航控制算法中的属性。它通过模型引用来引用设计模型，使得原有的设计模型保持不变。模块替换规则指定检查是否可能发生溢出的属性。验证子系统指定了属性证明时对速度输入范围的假设。该模型配置 Simulink Design Verifier 以将模块替换应用于 Sum 模块，该模块为引用模型中的定点 PI 控制器的输出端口提供数据，并返回演示溢出的反例。
使用 Observer Reference 模块进行属性证明分析
使用 Observer Reference 模块执行属性证明分析。
使用 Requirements Table 模块证明属性
使用 Requirements Table 模块和 Simulink Design Verifier 来证明模型的属性。
