使用 Requirements Table 模块证明属性
此示例显示如何使用 Requirements Table 模块和 Simulink® Design Verifier™ 来证明发动机推力反向系统的属性。
当您使用 Requirements Table 模块和 Simulink Design Verifier 进行属性证明时：
模块中的每个需求都定义了一个正式需求，您可以使用它来测试模型、子系统或模块的属性。在此示例中，Requirements Table 模块需求表示为预条件和后条件。
模块中的每个需求都会在需求编辑器中产生一个对应的需求。请参阅配置形式化需求的属性。
Simulink Design Verifier 为需求集中的需求生成证明目标。后条件定义了您通常在 Proof Objective (Simulink Design Verifier) 模块中定义的逻辑条件。仅当前提条件为真时，该模块才会评估与后置条件相关的证明目标。
有关详细信息，请参阅使用 Requirements Table 模块创建正式需求和使用 Simulink Design Verifier 证明模型属性 (Simulink Design Verifier)
查看 Requirements Table 模块中的需求
打开示例模型，property_proving_reqtable。在此示例中，您将测试发动机推力反向系统的属性，该系统由图 ThrustReverserDeployLogic 建模。Requirements Table 模块使用图输入信号和部署输出信号来观察图行为。该模块以表达式定义数据来评估图的输入和输出。请参阅在 Requirements Table 模块中定义数据。
要查看与每个需求相关的验证逻辑，请打开 Requirements Table 模块。这些需求与示例 通过分析模型属性来验证需求 (Simulink Design Verifier) 中使用的需求集的需求相对应。该模块证明了以下属性：
如果空速大于 150 节，则推力反向不得展开。
根据车轮重量传感器的数值显示，如果飞机在空中，推力反向不得展开。如果飞机在空中，两个车轮重量 (WOW) 传感器各自的信号值为
false。如果任一推力传感器的值为正，则推力反向不得展开。
如果起落架轮子的转速低于阈值，则推力反向不得展开。
每个需求定义一个属性。如果预条件有效，则后置条件也必须满足才能证明属性。
证明属性
为了证明属性，请在 Design Verifier 选项卡中点击证明属性。在这个示例中，图的属性得到了证明。Requirements Table 模块以绿色突出显示与已证明的证明目标相关的后条件。
如果需求证明目标被证伪，模块会用红色突出显示该需求。否则，如果 Simulink Design Verifier 无法证明或反驳证明目标，则该模块将以黄色突出显示该需求。您可以通过将此示例中的图替换为 通过分析模型属性来验证需求 (Simulink Design Verifier) 示例中使用的图的第一次迭代来研究此行为。
另请参阅
主题
- 证明模型中的属性 (Simulink Design Verifier)
- 使用 Requirements Table 模块创建正式需求
- 从 Requirements Table 块生成并导出测试
