概述

在此示例中，您分析了基于引擎推力倒车系统的四个要求的模型属性。物业分析的伪造结果表明，系统设计要求不完整 - 系统允许行为违反以下几个要求：

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

分析安全性能

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

安全性属性子系统是Simulink®DesignVerifier™库的验证子系统块。金宝app安全性属性中的验证逻辑对安全要求建模。例如，空速需求通过：

有关验证子系统块的更多信息，请参见验证子系统（金宝appSimulink设计验证者）。

2.查看要求。在模型中，单击显示观点右下方的图标，然后选择要求。这要求窗格打开。扩张throust_reverser_safety_requirments。

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

3.显示要求的验证状态。右键单击浏览器中的要求之一，然后选择验证状态。这经过验证列表示要求不执行。

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

属性分析完成后，单击刷新按钮以更新状态经过验证柱子。结果表明，四分之三的目标是伪造的 - 分析发现了伪造属性的信号条件，因此违反了要求。

用反例分析模型行为

从“设计验证结果结果摘要”窗口中，单击html打开详细的分析报告。在第4章中，每个伪造的属性列出了反例。例如，在伪造空速要求的反例中：

反示例时间序列表明在模拟中可能难以遇到的条件，但是导致模型行为违反了要求。通过分析反例中的信号依赖性来研究行为：

1.在设计验证者选项卡，单击模型中的亮点按钮。

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

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

4.在模型中提高一个级别，安全性能子系统。逐步浏览反例模拟时间。在里面模拟选项卡，单击退后。

5.在t = 0.1时，平均空速低于阈值，并且部署了推力反向器。在t = 0.2的情况下向前走，平均空速高于阈值，并且推力反向器仍被部署。这违反了要求。

伪造的属性和依赖性分析表明，控制系统算法是不完整的，并且要求不完整。

分析重新设计的系统

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

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

其他设计要求指出，推力反向器应在暂停后部署。重新设计的模型包括：

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

1.在模型中，从应用选项卡，单击需求经理。

2.在要求选项卡，单击要求编辑。

3.打开throust_reverser_safety_requirments在里面要求编辑。

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

5.新链接出现在需求编辑中，细节窗格，下链接。

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

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

在修订模型上运行属性分析。查看需求窗格中的结果。

结果表明属性是有效的。