有些需求很难通过基于模拟的测试来完全验证。
让我们用简化的飞机逆推力系统的四个要求来演示。逆推力装置用于飞机着陆后在跑道上减速。
我们需要确保在某些不安全的情况下不使用反推力装置。因此，有四个安全要求，规定了何时禁止反推器的部署。
注意到每个需求中都使用了“shall not”吗?在需求中使用“不得”可能表明需求很难完全验证。你怎么能确定你已经把异常情况考虑进去了呢?
使用基于模拟的测试，如果可能的话，我们将需要创建很多很多的测试用例来实现这个目标!
这就是性质证明的作用。
使用Simulink Design Veri万博1manbetxfier进行属性证明是一种静态分析技术，它使用形式化方法来证明给定属性是否始终有效。这种技术可以帮助您正式验证在设计中实现的特定需求总是得到满足。
本视频将带您通过一个示例，向您展示如何使用Simulink设计验证器和Simulink Check中的模型切片器功能正式验证这四个逆推力器安全万博1manbetx要求，并调试自动生成的反例。
该Simu万博1manbetxlink模型包含在statflow状态图中定义的逻辑，以确定飞机着陆后何时部署逆推力器。
定义了四个属性以验证安全要求;每个需求一个属性。属性已经在验证子系统中定义，该子系统不生成代码。属性可以使用Simulink块、statflow状态图或MATL万博1manbetxAB函数块中的MATLAB代码来定义。
让我们以车轮重量(Weight-on-Wheels)需求的属性为例。车轮重量(Weight-on-Wheels，简称“WOW”)传感器用于确定飞机何时在地面上。
WOW安全需求的属性描述显示为Verification子系统中的Annotation:“如果两个WOW传感器为假，则部署不能为真。”换句话说，如果飞机在空中，反推力装置就不应该展开。
WOW属性定义使用Simulink设计验证器库中的隐含块。万博1manbetxImplies块允许您指定一个条件来产生给定的响应。还使用了Simulink模型验证库中的断言块，它让Simu万博1manbetxlink设计验证器知道已定义了属性。
让我们在属性证明模式万博1manbetx中运行Simulink设计验证器，以验证设计是否满足所有四个安全要求。
万博1manbetxSimulink Design Verifier能够使四个属性中的三个失效。
每个属性违反的反例测试向量已经为调试自动生成。
反例可能很难调试，因为Simulink Design Verifier将尝试在尽可能少的时间步骤内找万博1manbetx到违规，并且该工具不了解整个系统中实际的物理情况。
你需要提供工程洞察力。一种方法是使用证明假设来限制信号的范围、变化率或其他特征。万博1manbetxSimulink Design Verifier在分析模型时将使用这些假设。
我们现在还不想增加假设，也不排除任何可能性。
相反，让我们使用Simulink Check中的Model Slicer来万博1manbetx调试反例。让我们从WOW属性开始。
这就像在WOW属性子系统中选择断言块一样简单，然后在设计验证器结果窗口中单击“调试”。
模型切片器会自动设置，以帮助我们逐步完成WOW属性的反例。
模型切片器允许您逐步进行模拟，以查看模型的哪些部分是活动的，以及在模拟中的任何步骤中信号值是什么。
如果我们后退一步，然后通过简短的反例模拟，我们可以看到有一个特定的瞬态条件，其中空速和轮速传感器值的突然变化可能违反WOW要求。这是一个不寻常的场景，但代表了在基于模拟的测试中很难定义的条件类型。
在分析了其他属性的反例后，并利用我自己设计类似逻辑的工程经验，我可以看到该设计没有充分考虑着陆后信号值的突然变化。
我们有很多方法可以解决这个问题。我决定增加一个新的要求，这将增加一个短的延迟，使逆推力器部署后，适当的条件得到满足。这种短暂的延迟不会影响反推器的物理性能。
让我们打开固定模型并再次运行属性证明。
都准备好了!
本例展示了如何使用Simulink Design Verifi万博1manbetxer和Simulink Check中的Model切片器来使用属性证明来分析安全需求并调试反例。
您还可以将证明目标链接到“需求工具箱”中的需求，以管理属性证明的验证结果，以及基于模拟的测试。
访问Simulink万博1manbetx设计验证器产品页面或Simulink检查产品页面以请求试用。
