概述

在本例中，您将分析基于发动机逆推力系统的四个需求的模型属性。来自属性分析的伪结果表明系统设计需求是不完整的——系统允许违反以下几个需求的行为:

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

安全性能分析

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

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

有关验证子系统块的详细信息，请参见验证子系统．

2.查看需求。在模型中，单击显示透视图图标，然后选择需求．的需求窗格中打开。扩大thrust_reverser_safety_requirements．

安全需求链接到安全属性子系统中的断言块。断言块被认为是证明目标。每个需求的验证状态反映了其对应断言块的属性分析结果。

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

4.分析模型属性。在应用程序选项卡上,单击设计验证器．在设计验证器选项卡上,单击证明属性．

属性分析完成后，单击刷新控件中的状态验证列。结果表明，四个目标中有三个是伪造的——分析发现了一个伪造属性的信号条件，因此违反了要求。

用反例分析模型行为

在“设计验证器结果摘要”窗口中，单击超文本标记语言打开详细的分析报告。在第4章中，每个被证伪的属性都列出了一个反例。例如，在反例中伪造了空速要求:

反例时间序列表明在模拟中可能难以遇到的条件，但仍然会导致违反需求的模型行为。通过分析反例中的信号依赖关系来调查行为:

1.在设计验证器选项卡，单击模型高亮显示按钮。

2.属性中的航速有效断言块>安全属性>空速属性子系统。

3.在设计验证器选项卡，单击使用切片器调试按钮。该模型突出显示空速有效断言的依赖关系，并显示T = 0.2时的信号值。

4.在模型中向上移动一层，到安全属性子系统。回溯反例模拟时间。在模拟选项卡上,单击退一步．

5.当T = 0.1时，平均空速低于阈值，反推器展开。往前推，在T = 0.2时，平均空速高于阈值，反推器仍在展开。这违反了一个需求。

伪性和相关性分析表明控制系统算法设计不完整，需求不完整。

分析重新设计的系统

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

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

附加的设计要求规定，逆推力器应在暂停后展开。重新设计的模型包括:

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

1.在模型中，从应用程序选项卡上,单击要求经理．

2.在需求选项卡上,单击要求编辑器．

3.开放thrust_reverser_safety_requirements在要求编辑器．

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

5.新的链接出现在需求编辑器中，在右边的窗格中链接．

6.删除到原始模型中断言块的链接。如果原始模型是关闭的，则此链接似乎无法解决。在链接旁边，单击删除链接图标。

7.在重新设计的模型中重复其他三个需求和验证块。

在修改后的模型上运行属性分析。在Requirements窗格中查看结果。

结果表明，这些性质是有效的。