Pat Canny,MathWorks
用Simulink设计验证器进行性能验证™ 金宝app是一种静态分析技术,它使用形式化方法来证明给定属性是否始终有效。此技术可以帮助您正式验证设计中实现的特定需求是否始终得到满足。如果某个属性无效,将自动生成一个反例进行调试。
学习如何使用Simulink Design Verifier执行属性证明,并查看如何使金宝app用Simulink Check™的modelslicer工具调试自动生成的反例。
有些需求很难通过基于仿真的测试完全验证。
让我们用简化飞机反推系统的四个要求来演示。反推装置用于飞机着陆后在跑道上减速。
我们需要确保在某些不安全条件下不会部署反推装置。因此,有四项安全要求规定了何时禁止部署反推装置。
请注意,在每个要求中使用“不应”?在要求中使用“不应”可能表明该要求很难完全验证。您如何确定您已经解释了异常情况?
使用基于模拟的测试,我们需要创建很多很多测试用例来实现这个目标,如果这是可能的话!
这是财产证明可以提供帮助的地方。
Simulink Design Verifi金宝apper属性证明是一种静态分析技术,它使用形式化方法证明给定属性是否始终有效。此技术可以帮助您正式验证设计中实现的特定需求是否始终得到满足。
本视频将向您介绍一个示例,该示例演示如何在Simulink Check中使用Simulink Design Verifier和模型切片器功能,金宝app以正式验证这四个反推装置安全要求,并调试自动生成的反例。
该Simu金宝applink模型包含状态流状态图中定义的逻辑,用于确定飞机着陆后何时部署反推装置。
定义了四个属性,以验证安全要求;每个需求一个属性。属性已在验证子系统中定义,该子系统不生成代码。可以使用Simulink块、状态流状态图或MATLAB功能块中的MATLAB代码定义属性。金宝app
让我们以车轮重量需求的属性为例。轮子上的重量,或“哇”,传感器用于确定飞机何时在地面上。
WOW安全要求的属性描述在验证子系统中显示为注释:“如果两个WOW传感器为假,则部署不可能为真。”换句话说,如果飞机在空中,则不应部署反推装置。
WOW属性定义使用Simulink设计验证程序库中的Implies块。Implies块允许您指定一个条件来生成给定的响金宝app应。还使用Simulink模型验证库中的断言块,它让Simulink Design Verifier知道已定义属性。
让我们在属性验证模式金宝app下运行Simulink Design Verifier,以验证设计是否满足所有四个安全要求。
金宝appSimulink设计验证程序能够使四个属性中的三个无效。
为调试自动生成了每个属性冲突的反例测试向量。
反例可能很难调试,因为Simulink Design Verifier将尝试在尽可能少的时间步内找到金宝app冲突,并且该工具对整个系统中的实际情况一无所知。
您需要提供工程洞察力。一种方法是使用验证假设来限制信号的范围、变化率或其他特性。Simulink设计验证人在分析模型时将使用这些假设。金宝app
我们还不想添加假设,以免排除任何可能性。
相反,让我们使用Simulink Check中的模型切片器来调试一个反例。金宝app让我们从魔兽世界属性开始。
这非常简单,只需在WOW属性子系统中选择断言块,然后在Design Verifier结果窗口中单击“调试”。
模型切片器会自动设置,以帮助我们逐步完成WOW属性的反例。
模型切片器允许您逐步完成模拟,以查看模型的哪些部分处于活动状态,以及模拟中任何步骤的信号值。
如果我们通过简短的反例模拟后退一步,然后前进一步,我们可以看到有一个特定的瞬态条件,其中空速和轮速传感器值的突然变化可能违反WOW要求。这是一个不寻常的场景,但代表了在基于模拟的测试中难以定义的条件类型。
在分析了其他属性的反例后,并利用我自己设计类似逻辑的工程经验,我可以看出,该设计没有充分考虑着陆后信号值的突然变化。
我们有很多方法可以解决这个问题。我决定增加一个新的要求,在适当的条件得到满足后,增加一个短暂的延迟来启用反推装置。这个短暂的延迟不会影响反推装置的物理性能。
让我们打开固定模型并再次运行属性验证。
准备就绪!
该示例演示了如何使用Simulink检查中的Simulink设金宝app计验证器和模型切片器来使用属性证明来分析安全需求和调试反例。
除了基于模拟的测试外,您还可以将验证目标与Simulink需求中的需求相链接,以管理属性验证的验证结果。金宝app
访问Simulink金宝app Design Verifier产品页面或Simulink Check产品页面以请求试用。
您还可以从以下列表中选择网站:
选择中国站点(中文或英文)以获得最佳站点性能。其他MathWorks国家/地区网站未针对您所在地的访问进行优化。