Main Content

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

防抖动时间属性

打开脚本

此示例展示了如何使用 Simulink® Design Verifier™ Temporal Operator 模块来模型属性证明和测试用例生成的时间系统需求。

时间运算符

Simulink® Design Verifier™ 库提供了三个基本的时间操作符模块，可用于对时间属性模型。时间运算符的目的是支持时间需求的规范，使得建模的属性与实际的文本需求具有更紧密的相互关系。这些模块是用于构建更复杂的时间属性的低级构建模块。

防抖模型和需求

考虑一个去抖动逻辑，该逻辑根据输入在固定数量的时间步中保持的值，在 0 和 1 之间的值之间进行去抖动。

包含的 Stateflow ® 图表中捕获了去抖动功能。

open_system('sldvdemo_debounce_to')
open_system('sldvdemo_debounce_to/debounce')

考虑您想要验证的去抖动模型的两个需求。

需求 1：

每当输入等于 1 且超过 6 步时，输出应等于 2。

需求 2：

每当输出为 2 后，输入变为 0 超过 5 步时，只要输入保持为 0，输出就等于 1。

属性规范

为了指定需求 1，您首先要表示约束，即输入等于 1 且超过 6 步。这可以通过时间操作符模块库中的 Detector模块捕获。当检测到输入值为 1 且持续 7 个（或超过 6 个）时间步长时，您需要检查只要检测后输入保持等于 1，输出是否等于 2。使用 Detector模块的“同步”选项，后跟 Implies模块来捕获此信息。

open_system('sldvdemo_debounce_to/Verify True Output1')

可以组合多个时间操作符模块来构建更复杂的时间属性。考虑需求 2。

open_system('sldvdemo_debounce_to/Verify True Output2')

为了说明起见，这个需求大致分为三个部分：

  1. 输出结果为 2之后：这是您获得属性的有利条件。在检查其余约束时，您想知道这个条件在过去的某个时间点是否为真。这种类型的启用条件通常后面跟着一个扩展器（“有限”或“无限”），它与其他约束结合，可能形成您蕴涵的第一个输入。

  2. 输入变为 0 超过 5 步并且只要输入保持为 0就检查某些内容：出于与第一个属性相同的原因，您使用具有“同步”输出的检测器（“输入检测的时间步长”= 6）。

  3. 输出应等于 1：当前两个约束成立时，您想要验证的条件就是这个。这是通过逻辑Implies模块捕获的。请注意，您不能在这里使用Within Implies模块。

属性证明

一旦对时间需求进行了建模，您就可以使用 Simulink Design Verifier 对其执行属性证明。

清理

为了完成示例，请关闭所有打开的模型。

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_debounce_to',0);