主要内容

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

指定 SimulinkStateflow 元素的输入范围

当您对 Simulink® 和 Stateflow® 元素指定输入范围约束时,Simulink Design Verifier™ 会在分析过程中考虑这些约束。

指定 Inport 模块的输入范围

在 Inport 模块上指定输出最小值和最大值后,Simulink Design Verifier 分析将使用最小值和最大值作为约束。

以下示例模型限制来自两个 Inport 模块的信号:

  • 输入 1 模块:最小值:1、最大值:5

  • 输入 2 模块:最小值:-1,最大值:1

当您使用 Simulink Design Verifier 分析此模型时,分析将产生以下结果:

  • Input1 的输出永远不会小于 0,因此 Logical Operator 模块的第一个输入永远不会是 false。逻辑运算符的第一个输入等于 false 的目标是无法满足的。

  • Logical Operator 模块无法实现 100%修正条件/决策覆盖率 (MCDC),因为第一个输入为 false 的条件从未发生。

详细的分析报告显示了您用作输入 1 和输入 2 约束的值。

注意

Simulink Design Verifier 仅考虑根级输入的最小和最大约束值。

指定 Simulink.Signal 对象的输入范围

使用模型浏览器,在模型工作区中,您可以指定与输入信号相关的 Simulink.Signal 对象的最小值和最大值

以下示例模型使用与输入信号 ab 相关的 Simulink.Signal 对象来限制信号值:

  • 信号 a:最小值:1、最大值:5

  • 信号 b:最小值:-1,最大值:1

当您分析此模型时,结果与您在输入端口上指定最小值和最大值相同。

指定 Inport 模块和信号上的信号范围

如果您在 Inport 模块和信号上指定范围,则分析会考虑值的最小范围。例如,如果您在输入端口上指定 4..12 的范围,并在来自输入端口的信号上指定 1..8 的范围,则分析会考虑范围 4..8

指定 Stateflow 数据对象的输入范围

使用模型资源管理器,您可以为 Stateflow 图指定直接连接到根级输入端口的数据对象的范围

在下面的示例模型中,名为 Chart 的 Stateflow 图具有一个数据对象 x,其范围指定为 0 < x < 10。在此图中,x 必须大于 15 才能触发从 lowhigh 的转移。

x 的值范围从 0 到 10,因此转移条件 [x > 15] 永远不会是 true。从 lowhigh 的转移从未发生。因为从未进入 high 状态,所以从未测试转移条件 [x < 15],并且从未发生从 highlow 的转移。图始终处于 low 状态。

当您分析这个模型时,这些目标被证明是无法满足的:

  • 从未进入 high 状态。

  • 转移条件 [x > 15] 始终是 false,从来不是 true

  • 条件 [x < 15] 从未被测试过,所以它永远不会是 truefalse

分析报告指出您用作 x 约束的值:[0, 10]。

指定子系统的输入范围

Simulink Design Verifier 软件仅将指定的输入最小值和最大值视为模型顶层的约束。您可以在子系统的输入端口上指定最小值和最大值,但是当您分析顶层模型时,软件会忽略这些值。

当您执行子系统分析时,软件会考虑子系统输入端口上指定的最小值和最大值。

例如,考虑以下模型及其子系统。

在子系统中,输入端口 SSIn 的指定最小值和最大值分别为 -10 和 10。Saturation 模块的下限和上限分别为 -15 和 15。

如果在顶层模型中右键点击子系统并选择Design Verifier > 生成子系统测试,分析会将指定的最小值和最大值视为对 SSIn 端口的约束。

约束:设计最小最大约束

分析发现有两个无法满足的目标:

  • 输入 > 下限 F:输入始终大于 Saturation 模块的下限 (-15)。

  • 输入 >= 上限 T:输入永远不会大于或等于 Saturation 模块的上限 (15)。

如果分析包含子系统的模型,则分析不会考虑子系统中输入端口 SSIn 上指定的值。该分析仅考虑层次结构相应级别的根级输入端口进行分析。

指定全局数据存储的输入范围

数据存储器是一个存储库,您可以向其中写入数据,也可以从中读取数据,而无需将输入或输出信号直接连接到数据存储器。您可以使用 Data Store Memory 模块或 Simulink.Signal 对象创建数据存储。您可以为任何数据存储指定最小值和最大值

在子系统分析期间,Simulink Design Verifier 创建一个输入端口来模拟全局数据存储的执行上下文。有关详细信息,请参阅 提取子系统进行分析。如果数据存储已指定最小值和最大值,则这些值将被分配为新输入端口上的最小值和最大值。Simulink Design Verifier 分析将输入的最小值和最大值视为子系统级分析约束。

在下面的示例模型中,数据存储 A 的最小值为 0,最大值为 10。

原子子系统从数据存储中读取值并检查输入是否小于 0。如果输入小于 0,则 Compare To Zero 模块输出 1,如果输入大于或等于 0,则输出 0。Test Objective 模块检查输出是否为 1。

在顶层模型中,如果右键点击子系统并选择Design Verifier > 生成子系统测试,则分析会将数据存储 A 的约束视为 [0, 10]。

该分析不满足 Test Objective 模块中指定的目标。输入始终大于或等于 0,因此 Compare To Zero 模块的输出始终为 0。

指定总线元素的输入范围

定义总线时,您可以指定总线中元素的最小值和最大值Simulink Design Verifier 在分析使用总线作为输入信号的子系统和模型时会考虑这些最小值和最大值。

考虑一个输入三个字段的总线的子系统,每个字段都有定义的最小值和最大值。要查看该子系统,请将示例文件夹添加到当前 MATLAB 路径,然后在命令行中输入:

open_system('sldvBusMinMaxExample');

总线元素总线元素最小值总线元素最大值
vehicleSpeed0125
throttle0100
engineSpeed07600

该子系统的测试目标为确认每个元素不超过常数。vehicleSpeed 信号被限制为低于测试目标的最大值。

将当前文件夹设置为可写文件夹。在顶层模式下,右键点击子系统并选择 Design Verifier > 生成子系统测试。由于 vehicleSpeed > 135 元素的最大规格,测试 vehicleSpeed 的条件目标无法满足。

使用指定的输入最小值和最大值作为约束

此示例展示了如何在测试生成和属性证明期间使用输入端口最小值和最大值作为 Simulink® Design Verifier™ 的分析约束。

该模型已预先配置为生成 MCDC 测试。指定的最小值和最大值显示在方括号中。本例中的约束使得一些覆盖率目标无法得到满足。当您生成测试而不考虑这些约束时,所有覆盖率目标都会得到满足。

1.Input1 和 Input2 的最小值和最大值直接在其各自的输入端口信号属性上捕获。

2.最小值和最大值在与信号 a 和 b 相关的 Simulink.Signal 对象上指定。Simulink Design Verifier 使用信号对象的值作为约束。当指定多个最小值和最大值时(例如在输入端口和信号对象上),Simulink Design Verifier 会考虑它们最紧的范围。

3.Simulink Design Verifier 考虑直接连接到根级输入端口的 Stateflow® 数据上指定的最小和最大限制范围

4.对于子系统分析,考虑子系统根级指定的输入最小值和最大值。观察到,为子系统生成测试使用了在 SSIn 上指定的约束,但在系统级分析中忽略了它们。

open_system('sldvdemo_minmaxconstraints');