Main Content

指定并验证设计需求

根据需求验证设计，使用输入假设优化反例

安全需求定义模型中的意外行为。Simulink® Design Verifier™ 使用属性证明来验证与模型需求相关联的属性在所有可能的输入值下是否成立，或者提供导致违规的反例。您可以使用 Simulink Design Verifier 将设计需求建模为属性，然后证明模型中的属性。

模块

全部展开

Proof Assumption在证明模型属性时约束信号值
Proof Objective定义信号在证明模型属性时必须满足的目标
Assertion检查信号是否为零
Detector检测输入的真实持续时间并根据输出类型构建输出的真实持续时间
Extender延长输入的真实时长
Implies指定产生特定响应的条件
Within Implies验证响应是否在所需时间内发生
Verification Subsystem指定证明或测试目标而不影响仿真结果或生成的代码

函数

全部展开

sldv.assumeStateflow 图表和 MATLAB 函数模块的证明假设函数
sldv.proveStateflow 图表和 MATLAB 函数模块的证明目标函数
sldvextract将子系统或子图内容提取到新模型中进行分析
sldvoptions创建设计验证选项对象
sldvrun分析模型
sldvreport生成Simulink Design Verifier报告

主题

入门知识

用于验证和确认的需求建模

通过属性证明进行验证

  • 证明模型中的属性
    提供一个示例，引导您完成证明模型属性的过程。
  • 设计和验证模型中的属性
    您可以使用 Simulink® Design Verifier™ 将设计需求模型为属性，然后在模型中证明属性。要验证与模型需求相关的属性在所有可能的输入值下是否成立，请使用属性证明分析。如果需求失败，Simulink Design Verifier 会提供反例来调试失败。
  • 使用模型切片器调试属性证明违规行为
    使用 Model Slicer 通过断言模块调试您的设计。
  • 使用验证模型证明系统级属性
    使用验证模型来证明系统级属性的示例。
  • 证明子系统中的属性
    解释如何证明子系统中的属性。
  • 检查指定的最小值和最大值违规
    描述如何分析模型以验证是否遵守指定的设计最小值和最大值。
  • sldvData 字段中输入范围的规范
    描述最小和最大输入值的 sldvData 字段。
  • 使用 MATLAB 函数模块进行属性证明
    此示例说明如何验证安全带提醒器设计模型。其下方的安全属性模块包含 MATLAB ® 中指定的属性，用于指示图标何时应处于活动。Simulink ® Design Verifier™ 分析设计模型和安全属性以证明正确性或识别反例。在该模型中，该属性被违反，因为设计隐式假设 KEY 输入从 0 开始并以 1 的增量变化。
  • 使用 MATLAB Truth Table 模块进行属性证明
    此示例显示如何验证上面顶部模块中引用的安全带提醒设计模型。其下方的安全属性模块包含 MATLAB 真值表中指定的属性，该属性指示 SeatBeltIcon 输出何时应处于活动。Simulink Design Verifier 分析设计模型和安全属性以证明正确性或找出反例。在该模型中，该属性是在明确假设 KEY 输入从 0 开始并以 1 的增量变化的情况下证明的。
  • 使用假设模块证明属性
    此示例显示如何使用 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 给出了一个反例来证明违规行为。
  • 证明大型模型中的属性
    描述证明大型模型中的属性的工作流程和最佳实践。