模型需求
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 信号也变为真。只要 CMD 为真，SENSOR_HIGH 就为真，除非该模块被 MANUAL_RESET 信号重置。
延伸真实信号
在此示例中，输入变为真后，输出也将在 Detector 模块中指定的时间步数内变为真，在本例中为 5。输入对于 5 个时间步同样保持真实。
根据指定阈值测试输入
当输入 In3 等于 ON 且输入 In4 小于常数 THRESHOLD 时，In3 在五个时间步内设置为 OFF。
