主要内容

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

检查指定的最小值和最大值违规

在设计错误检测分析期间,软件会检查整个模型的中间信号和输出端口上指定的最小值和最大值。这些值定义了设计范围

分析检查指定的最小值和最大值:

  • Simulink® 模块输出,但下一节中描述的限制除外

  • Simulink.Signal 对象

  • Stateflow® 数据对象

  • MATLAB® 用于代码生成数据对象

  • 全局数据存储写入

如果分析检测到信号超出了设计范围,结果将确定模型中出现错误的位置。此外,您还可以生成一个包含测试用例的框架模型,这些测试用例可以演示错误是如何发生的。

检查指定最小值和最大值违规的限制

要分析模型检查是否超出指定的最小值和最大值,请选择设计错误检测窗格中信号范围错误下的指定的最小值和最大值违规

该软件无法检查以下指定的最小值和最大值:

  • 任何 Mux 模块,其输出连接到 Selector 模块

  • Merge 模块输入

    要解决此限制,请在 Merge 模块输出上使用 Simulink.Signal 对象并在 Simulink.Signal 对象上指定范围。

注意

有关 Simulink Design Verifier™ 分析如何处理输入端口上指定的最小值和最大值的信息,请参阅 最小和最大输入约束

关于此示例

在本节中,您将创建并分析一个模型,该模型具有指定的设计最小值和最大值:

  • 输入端口

  • 两个中间模块的输出端口

设计错误检测分析可识别输出值超出设计范围的模块。如果分析检测到此错误,此示例将演示分析如何在继续分析时使用指定的最小值和最大值。

创建示例模型

为此示例创建模型:

  1. MATLAB 工具条的主页选项卡上,选择 新建 > Simulink 模型

  2. 从 Simulink 常用模块库中,将以下模块添加到模型并分配指示的参数值。

    模块选项卡参数
    Inport信号属性最小值0
    Inport信号属性最大值5
    Gain主要增益5
    Gain信号属性输出最小值0
    Gain信号属性输出最大值20
    Gain信号属性输出数据类型int16
    Saturation主要上限25
    Saturation主要下限-25
    Saturation信号属性输出最小值-25
    Saturation信号属性输出最大值25
    Outport没有变化
  3. 按照图示连接四个模块。

  4. 要显示指定的最小值和最大值,请在调试选项卡上选择 叠加信息 > 信号数据范围

  5. 建模选项卡上,点击模型设置

  6. 在“配置参数”对话框的求解器窗格中,在求解器选择下:

    1. 类型设置为定步长

      Simulink Design Verifier 软件不支持可变步长求解器。

    2. 求解器设置为离散(无连续状态)

  7. Design Verifier 窗格上,将模式设置为设计错误检测

  8. Design Verifier > 设计错误检测窗格上:

    1. 选择指定的最小值和最大值违规

    2. 清除整数溢出除以零参数。

    在此示例中,您仅检查中间的最小违规和最大违规。

  9. 要保存这些设置并退出“配置参数”对话框,请点击确定

  10. 保存模型并将其命名为 ex_interim_minmax

分析模型

为了分析示例模型来识别任何违反指定最小值和最大值的中间信号,执行设计错误检测分析。

Design Verifier 选项卡上,点击检测设计错误

分析完成后:

  • 该软件通过分析结果突出显示模型。

  • Simulink Design Verifier 结果对话框打开并显示分析摘要。

查看分析结果

审查模型结果

在模型窗口中,Gain 模块为红色,Saturation 模块为绿色。这表明:

  • Gain 模块相关的目标至少有一个被伪造。对于此示例,分析恰好证伪了一个目标。

  • Saturation 模块相关的所有目标都已满足。对于此示例,分析恰好满足一个目标。

要理解这些结果:

  1. 点击 Gain 模块。

    Simulink Design Verifier 结果窗口显示输出的设计范围为 [0..20],但分析检测到错误并生成了一个演示该错误的测试用例。因为输入模块的设计范围是[0..5],所以当 Gain 模块的输入为 5 时,输出为 25,超过了该端口上指定的最大值。

    分析计算并显示派生范围,以帮助您了解超出设计范围的原因。

  2. 点击 Saturation 模块。

    Simulink Design Verifier 结果窗口显示 Saturation 模块的输出从未超出设计范围 [–25..25]。Saturation 模块的输入从未超过 [0..25],这是分析从 Gain 模块传播得出的范围。

审核框架模型

分析完成后,您可以创建一个包含导致错误的测试用例的框架模型。

对于示例模型,查看导致 Gain 模块中设计范围错误的测试用例:

  1. 分析完成且模型突出显示后,选择 Gain 模块。

  2. Simulink Design Verifier 结果窗口中,点击查看反例

    软件创建一个名为 ex_interim_minmax_harness 的框架模型,并打开框架模型中包含反例的 Signal Editor 模块。

    Signal Editor 模块中,一个测试用例(其信号值为 5)导致 Gain 模块的输出为 25,超过了指定的最大值 20

  3. 在仿真此测试用例之前,请在“配置参数”对话框的诊断 > 数据有效性窗格中将仿真范围检查设置为警告错误

    设置此参数可指定在仿真中当 Simulink 检测到信号超过指定的最小值或最大值时要采取的诊断措施。

    • 如果指定警告,诊断查看器将显示一条警告消息并继续。

    • 如果指定错误,诊断查看器将显示错误消息并停止。

  4. 点击确定保存更改并关闭“配置参数”对话框。

  5. 框架模型的工具条中,点击全部运行以使用此反例来仿真模型。

    正如预期的那样,仿真在 MATLAB 窗口中显示警告或错误,表示 Gain 模块的输出值超过了指定的最大值。

查看分析报告

您还可以生成一个 HTML 报告,其中包含有关 ex_interim_minmax 模型分析的详细信息。要创建此报告,请在 Simulink Design Verifier 结果窗口中点击 HTML。分析报告在浏览器中打开。

在分析报告中,报告的设计错误检测目标状态章节提供了两类详细的结果:

  • 目标证明有效 - Saturation 模块的输出值始终在设计范围内。

  • 用测试用例证伪的目标 - Gain 模块的输出值违反了设计范围。