概述

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

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

分析安全性质

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

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

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

2.查看需求。在模型中，单击显示角度的观点在右下角的图标，并选择需求．的需求窗格中打开。扩大thrust_reverser_safety_requirements.．

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

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

4.分析模型属性。在里面应用选项卡，单击设计验证者．在里面设计验证者选项卡，单击证明属性．

当属性分析完成后，单击刷新按钮更新状态验证列。结果显示，四分之三的目标是伪造的——分析发现了一个信号条件，篡改了属性，因此违反了要求。

分析模型行为与反例

从设计验证程序结果摘要窗口中，单击超文本标记语言打开详细的分析报告。在第4章中，每个伪造属性列出了一个反例。例如，在伪造空速要求的强调范围内：

ConsterExample时间序列表示模拟中可能难以遇到的条件，但仍然会导致违反要求的模型行为。通过分析CounterExample中的信号依赖性来调查该行为：

1.在里面设计验证者选项卡上,单击模型中突出显示按钮。

2.中选择空速有效断言块测试装置>安全性能>空速性能子系统。

3.在里面设计验证者选项卡上,单击使用Slicer调试按钮。该模型强调了空速有效断言的依赖性，并显示了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.删除原始模型中assert块的链接。如果原始模型是关闭的，那么这个链接似乎没有得到解决。在链接旁边，单击删除链接图标。

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

运行修订模型的财产分析。查看要求窗格的结果。

结果表明该属性有效。