Main Content

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

使用 Requirements Table 模块证明属性

自 R2023a 起

此示例使用:

打开模型

此示例显示如何使用 Requirements Table模块和 Simulink® Design Verifier™ 来证明发动机推力反向系统的属性。

当您使用 Requirements Table模块和 Simulink Design Verifier 进行属性证明时：

  1. 模块中的每个需求都定义了一个正式需求，您可以使用它来测试模型、子系统或模块的属性。在此示例中，Requirements Table模块需求表示为预条件和后条件。

  2. 模块中的每个需求都会在需求编辑器中产生一个对应的需求。参见 配置正式需求的属性 (Requirements Toolbox) 。

  3. Simulink Design Verifier 为需求集集中的需求生成证明目标。后条件定义了您通常在 Proof Objective 模块中定义的逻辑条件。仅当前提条件为真时，该模块才会评估与后置条件相关的证明目标。

有关更多信息，请参阅 使用 Requirements Table 模块创建正式需求 (Requirements Toolbox) 和 什么是财产证明？ 。

查看 Requirements Table 模块中的需求

打开示例模型，property_proving_reqtable。在此示例中，您将测试发动机推力反向系统的属性，该系统由图表 ThrustReverserDeployLogic 建模。Requirements Table模块使用图表输入信号和部署输出信号来观察图表行为。该模块以表达式定义数据来评估图表的输入和输出。参见 在 Requirements Table 模块中定义数据 (Requirements Toolbox) 。

要查看与每个需求相关的验证逻辑，请打开Requirements Table模块。这些需求与示例 通过分析模型属性来验证需求 中使用的需求集的需求相对应。该模块证明了以下属性：

  1. 如果空速大于 150 节，则推力反向不得展开。

  2. 根据车轮重量传感器的数值显示，如果飞机在空中，推力反向不得展开。如果飞机在空中，两个车轮重量（WOW）传感器各自的信号值为 false 。

  3. 如果任一推力传感器的值为正，则推力反向不得展开。

  4. 如果起落架轮子的转速低于阈值，则推力反向不得展开。

每个需求定义一个属性。如果预条件有效，则后置条件也必须满足才能证明属性。

证明属性

为了证明属性，请在Design Verifier选项卡中点击证明属性。在这个例子中，图表的属性得到了证明。Requirements Table模块以绿色突出显示与已证明的证明目标相关的后条件。

如果需求证明目标被证伪，模块会用红色突出显示该需求。否则，如果Simulink Design Verifier无法证明或反驳证明目标，则该模块将以黄色突出显示该需求。您可以通过将此示例中的图表替换为 通过分析模型属性来验证需求 示例中使用的图表的第一次迭代来调查此行为。

另请参阅

(Requirements Toolbox)

相关主题