Main Content

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

模型需求

Simulink® Design Verifier™模块库包含一个子库 Example Properties。示例属性子库包括：

  • 基本属性 — 四个例子说明如何证明基本属性。

  • 时间属性 — 四个示例演示如何定义布尔信号的时间属性

在您的模型中使用这些示例的工作流程是：

  1. 将这些示例复制到你的Verification Subsystem模块中。

  2. 如果需要，请根据您想要证明的特定属性对其进行调整。

  3. 运行Simulink Design Verifier分析来证明这些示例中的断言永远不会失败。

  4. 如果断言失败，软件会创建导致断言失败的反例，然后生成框架模型。

  5. 在线框架模型上，执行反例以确认断言因该反例而失败。

基本属性

要查看基本属性示例：

  1. 打开Simulink Design Verifier模块库。类型：

    sldvlib

  2. 双击 Examples 子库。

  3. 双击包含示例的 基本属性模块。

接下来的部分详细描述了 Block Properties 子库中的每个示例。

触发结果的条件

Simulink Design Verifier Implies模块允许您测试触发结果的条件。此示例指定如果条件 A 为真，则结果 B 必须始终为真。

增加或减少信号

本节中的两个示例指定信号是：

  • 始终增加或保持不变

  • 始终减少或保持不变

独家经营

此示例描述了四种不应同时成立的情况。

具有一个真元素的条件

此示例指定四个输入信号中只有一个可以为真。

时间属性

要查看时间属性示例：

  1. 打开Simulink Design Verifier模块库。类型：

    sldvlib

  2. 双击 Temporal Properties 子库。

  3. 双击包含示例的 Temporal Properties模块。

接下来的部分详细描述了时间属性子库中的每个示例。

使输出与输入同步

当输入的In1等于ACTIVE时，输入的In2在五个时间步后设置为INACTIVE。

延迟一段时间后使信号无效

在这个例子中，在 SENSOR_HIGH 输入为真的五个连续时间步之后，CMD 信号也变为真。只要 SENSOR_HIGH 为真，CMD 就为真，除非该模块被 MANUAL_RESET 信号重置。

延伸真实信号

在此示例中，输入变为真后，输出也将在 Detector模块中指定的时间步数内变为真，在本例中为 5。输入对于 5 个时间步同样保持真实。

根据指定阈值测试输入

当输入 In3 等于 ON 且输入 In4 小于常数 THRESHOLD 时，In3 在五个时间步内设置为 OFF。

相关主题