模型需求
Simulink® Design Verifier™模块库包含一个子库 Example Properties。示例属性子库包括:
在您的模型中使用这些示例的工作流程是:
将这些示例复制到你的Verification Subsystem模块中。
如果需要,请根据您想要证明的特定属性对其进行调整。
运行Simulink Design Verifier分析来证明这些示例中的断言永远不会失败。
如果断言失败,软件会创建导致断言失败的反例,然后生成框架模型。
在线框架模型上,执行反例以确认断言因该反例而失败。
基本属性
要查看基本属性示例:
打开Simulink Design Verifier模块库。类型:
sldvlib
双击 Examples 子库。
双击包含示例的 基本属性模块。
接下来的部分详细描述了 Block Properties 子库中的每个示例。
触发结果的条件
Simulink Design Verifier Implies模块允许您测试触发结果的条件。此示例指定如果条件 A
为真,则结果 B
必须始终为真。
增加或减少信号
本节中的两个示例指定信号是:
始终增加或保持不变
始终减少或保持不变
独家经营
此示例描述了四种不应同时成立的情况。
具有一个真元素的条件
此示例指定四个输入信号中只有一个可以为真。
时间属性
要查看时间属性示例:
打开Simulink Design Verifier模块库。类型:
sldvlib
双击 Temporal Properties 子库。
双击包含示例的 Temporal Properties模块。
接下来的部分详细描述了时间属性子库中的每个示例。
使输出与输入同步
当输入的In1
等于ACTIVE
时,输入的In2
在五个时间步后设置为INACTIVE
。
延迟一段时间后使信号无效
在这个例子中,在 SENSOR_HIGH
输入为真的五个连续时间步之后,CMD
信号也变为真。只要 SENSOR_HIGH
为真,CMD
就为真,除非该模块被 MANUAL_RESET
信号重置。
延伸真实信号
在此示例中,输入变为真后,输出也将在 Detector模块中指定的时间步数内变为真,在本例中为 5。输入对于 5 个时间步同样保持真实。
根据指定阈值测试输入
当输入 In3
等于 ON
且输入 In4
小于常数 THRESHOLD
时,In3
在五个时间步内设置为 OFF
。