帕特凯西,马诺斯
使用Simulink Design Veri万博1manbetxfier™证明的属性是一个静态分析技术,它使用正式方法来证明特定属性是否始终有效。此技术可以帮助您正式验证设计中实现的特定要求,将始终满足。如果属性无效,将自动生成一个反异行为以进行调试。
学习如何使用Simulink Design Verifier执行属性证明,并了解如何使万博1manbetx用Simulink Check™中的Model Slicer工具调试自动生成的反例。
有些需求很难通过基于模拟的测试完全验证。
让我们使用四个要求进行简化的飞机推力反向程序系统来证明。推力逆转器用于在着陆后慢动在跑道上减慢飞机。
我们需要确保反推力装置在某些不安全的情况下不会被打开。因此,有四个安全要求定义了何时禁止反推器部署。
注意到每个需求中“不应该”的用法了吗?在要求中使用“不得”可能表明该要求难以完全验证。你怎么能确定你解释了异常情况?
通过基于仿真的测试,我们需要创造许多,许多测试用例来完成这一目标,如果甚至可能!
这就是财产证明可以帮助的地方。
Simulink Design Verifi万博1manbetxer特性证明是一种静态分析技术,它使用形式化方法来证明给定的特性是否始终有效。此技术可以帮助您正式验证设计中实现的特定要求,将始终满足。
本视频将带你通过一个例子,展示了如何使用Simulink设计验证器和模型切片器功能在Simulink检查正式验证这四个推力反向安全要求和调试自万博1manbetx动生成的反例。
此Simu万博1manbetxlink模型包含状态流状态图中定义的逻辑,以确定在飞机降落后何时部署推力反向器。
已定义四个属性以验证安全要求;每个要求的一个属性。该属性已在验证子系统中定义,该子系统不会生成代码。可以使用MATLAB功能块中的Simulink块,emotefl万博1manbetxow状态图表,emoteflow状态图表或MATLAB代码来定义属性。
让我们以Weight-on-Wheels需求的属性为例。“轮子上的重量”,或“WOW”,传感器用来确定飞机何时到达地面。
哇安全要求的属性描述在验证子系统中显示为注释:“如果两个哇传感器是假的,则部署不能为真。”换句话说,如果飞机在空气中,则不应部署推力反向器。
WOW属性定义使用了Simulink设计验证器库中的Implies块。万博1manbetxImplies块允许您指定产生给定响应的条件。还使用了Simulink Model Verificati万博1manbetxon库中的Assertion块,它让Simulink Design Verifier知道已经定义了一个属性。
让我们在属性中运行S万博1manbetximulink设计验证程序,以验证设计是否正在满足所有四种安全要求。
万博1manbetxSimulink Design Verifier能够使四个属性中的三个无效。
为调试自动生成每个属性冲突的每个属性的测试向量。
EnterneRexamples可能很难调试,因为Simulink Design Verifier将万博1manbetx尽可能少的时间步骤查找违规,并且该工具没有任何了解整个系统中的物理上现实的内容。
您需要提供工程洞察力。这样做的一种方法是使用证明假设来限制信号的范围,变化率或其他特征。万博1manbetxSimulink Design Verifier将在分析模型时使用这些假设。
我们不想添加假设,而不是统治任何东西。
相反,让我们使用来自Simulink Check的Model Slicer万博1manbetx来调试反例。让我们从WOW属性开始。
这就像在WOW属性子系统中选择Assertion块一样简单,然后在Design Verifier结果窗口中单击“Debug”。
模型切片机自动设置为帮助我们逐步浏览WOW属性的ConteRexample。
模型切片机允许您逐步仿真,以查看模型的哪些部分是活动的,并且信号值在模拟中的任何步骤中。
如果我们退后一步,然后通过短的对手仿真,我们可以看到存在特定的瞬态条件,其中空速和车轮速度传感器值的突然变化可以违反哇要求。这是一个不寻常的场景,但代表了基于模拟的测试中难以定义的条件类型。
在分析另一个属性的反例后,通过使用自己的设计类似逻辑的工程经验,我可以看到设计没有充分占地登陆后信号值的突然变化。
我们有很多方法可以解决这个问题。我决定增加一个新的要求,这将增加一个短延迟,使推力反向部署后,适当的条件是满足。这个短暂的延迟不会影响推力反向器的物理性能。
让我们打开固定模型并再次运行属性。
都准备好了!
这个例子展示了如何使用Simulink Check中的Simu万博1manbetxlink设计验证器和模型切片器来使用特性证明来分析安全需求和调试反例。
您还可以在Simulink requirements中将证明目标链接到需求,以管理属性证明以及基于模拟的测试万博1manbetx的验证结果。
访问Simulink万博1manbetx Design Verifier产品页面或Simulink检查产品页面以请求试用。
你也可以从以下列表中选择一个网站:
选择中国网站(以中文或英文)以获取最佳网站性能。其他MathWorks国家网站未优化您的位置。