防抖动时间属性
此示例展示了如何使用 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')
为了说明起见,这个需求大致分为三个部分:
输出结果为 2之后:这是您获得属性的有利条件。在检查其余约束时,您想知道这个条件在过去的某个时间点是否为真。这种类型的启用条件通常后面跟着一个扩展器(“有限”或“无限”),它与其他约束结合,可能形成您蕴涵的第一个输入。
输入变为 0 超过 5 步并且只要输入保持为 0就检查某些内容:出于与第一个属性相同的原因,您使用具有“同步”输出的检测器(“输入检测的时间步长”= 6)。
输出应等于 1:当前两个约束成立时,您想要验证的条件就是这个。这是通过逻辑Implies模块捕获的。请注意,您不能在这里使用Within Implies模块。
属性证明
一旦对时间需求进行了建模,您就可以使用 Simulink Design Verifier 对其执行属性证明。
清理
为了完成示例,请关闭所有打开的模型。
close_system('sldvdemo_TOBlocks',0); close_system('sldvdemo_debounce_to',0);