通过分析模型属性来验证需求

概述

在此示例中，您将分析基于发动机推力反向系统的四个需求的模型属性。属性分析的伪造结果表明系统设计需求不完整——系统允许违反以下几项需求的行为：

为了更好地理解模型行为，您可以分析导致不良模型行为的时间序列输入的依赖关系，因为系统缺乏所需的控制逻辑。然后，分析通过属性分析的修改后的控制系统模型。

分析安全属性

1.点击打开模型按钮打开原始模型并创建示例文件的工作目录。

安全属性子系统是来自 Simulink® Design Verifier™ 库的 Verification Subsystem模块。安全属性中的验证逻辑对安全需求进行建模。例如，空速需求通过以下方式验证：

有关 Verification Subsystem 模块的更多信息，请参阅 Verification Subsystem 。

2.查看需求。在模型中，点击右下角的显示透视视图图标，并选择需求。将打开需求窗格。展开 thrust_reverser_safety_requirements 。

安全需求与安全属性子系统中的Assertion模块相关。Assertion 区模块被视为证明目标。每个需求的验证状态反映了其对应的Assertion模块的属性分析结果。

3.显示需求的验证状态。右键单击浏览器中的某个需求，并选择验证状态。已验证列表示需求尚未执行。

4.分析模型属性。在App选项卡中，点击Design Verifier。在Design Verifier选项卡中，点击证明属性。

当属性分析完成后，点击刷新按钮来更新已验证列中的状态。结果表明，四个目标中有三个是被证伪的——分析发现了伪造属性的信号条件，因此违反了需求。

用反例分析模型行为

在设计验证器结果摘要窗口中，点击HTML以打开详细的分析报告。在第 4 章中，每个被证伪的属性都列出了一个反例。例如，在证伪空速需求的反例中：

反例时间序列表示在仿真中可能很难遇到的情况，但却会导致违反需求的模型行为。通过分析反例中的信号依赖性来调查行为：

1.在Design Verifier选项卡中，点击在模型中突出显示按钮。

2.在测试单元 > 安全属性 > 空速属性子系统中选择空速有效断言模块。

3.在Design Verifier选项卡中，点击使用切片器调试按钮。该模型突出显示了空速有效断言的依赖性，并显示 T = 0.2 时的信号值。

4.在模型中向上移动一级，至安全属性子系统。回顾反例仿真时间。在仿真选项卡中，点击后退。

5.当 T = 0.1 时，平均空速低于阈值，推力反向展开。继续向前，在 T = 0.2 时，平均空速高于阈值，并且推力反向装置仍然处于展开状态。这违反了需求。

伪造属性和依赖性分析表明控制系统算法设计不完整，需求不完整。

分析重新设计的系统

重新设计控制系统需要重新考虑需求。在这种情况下，当输入突然改变时，缺少中间待机状态会导致不良的系统行为。添加一个延迟推力反向响应的中间部署模式可以解决这个问题。

打开reqs_validation_property_proving_redesigned_model模型。打开thrustReversers图表。

附加设计需求规定推力反向应在暂停后展开。重新设计的模型包括：

从重新设计的模型中的验证模块创建到需求的链接：

1.在模型中，从App选项卡中，点击需求管理器。

2.在需求选项卡中，点击需求编辑器。

3.在需求编辑器中打开thrust_reverser_safety_requirements。

4.对于需求 1.1“空速条件”，链接到安全属性 > 空速属性子系统中的空速有效模块。将 R1.1 从需求浏览器拖到模型中的空速有效模块。

5.新的链接出现在需求编辑器右侧窗格中的链接下。

6.删除原始模型中到断言模块的链接。如果原始模型已关闭，则此链接将显示为未解析。点击链接旁边的删除链接图标。

7.对重新设计的模型中的其他三个需求和验证模块重复上述操作。

对修改后的模型进行属性分析。在“需求”窗格中查看结果。

结果表明该属性是有效的。