Simulink Design Verifier

使用形式化方法进行错误检测

与仿真中的语义检查或分析不同,Simulink Design Verifier 使用的形式化方法可以发现特定动态运行情况是否会发生以及在什么条件下发生。这些信息可用于改进设计以及设计需求, 或用于辅助仿真调试和验证。Simulink Design Verifier 可以检测到以下常见设计错误:整数溢出、被零除、死逻辑和断言冲突。

检测整数溢出和被零除

您可以使用 Simulink Design Verifier 中的设计错误检测模式来发现整数溢出和被零除。此分析会自动执行,不需要额外的用户输入。它会提供所有模块的所有信号的允许范围,引导您找出问题的根本原因。最后,您可以直接在模型中查看结果,或生成 HTML 报告。

模型中的模块会标记为绿色、黄色或红色。绿色表示已经被证明不会导致整数溢出或被零除。黄色表示无法产生确定分析结论或超出分析时限的情况。如果在模型执行路径中发现错误,该路径中所有可显示整数溢出和被零除的后续块都将标记为黄色。

红色模块表示存在设计错误。Simulink Design Verifier 会为红色模块生成测试用例,可在仿真或测试中重现问题。您可以在 Simulink 中直接调用该测试用例并运行仿真。

检测死逻辑

您可以在 Simulink Design Verifier 中使用测试生成模式来检测死逻辑,即经证明在模型执行过程中永远不会被激活的模型部分。死逻辑通常因设计错误或需求错误而导致。在代码生成过程中,死逻辑会导致死代码。单独使用仿真测试难以检测到死逻辑,因为即使在运行大量仿真之后,仍然难以证明特定行为无法被激活。

在测试分析结束时,会根据测试标准为模型标记颜色。包含无法在仿真中激活的逻辑的模型对象标记为红色;包含可在仿真中完全激活的逻辑的模型对象标记为绿色。Simulink Design Verifier 会生成可在仿真过程中重现死逻辑的测试用例。

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Simulink Design Verifier 将 Stateflow 中的转移突出显示为红色。因为“press < zero_thresh”条件永远不可能为 false,所以这个转移条件导致了死逻辑。

检测断言冲突

Simulink Design Verifier 中提供了属性验证模式,您可以使用其中的冲突检测设置来检测断言冲突。在分析设定选项指定的仿真时间内,Simulink Design Verifier 会验证是否存在能触发断言的情况。例如,您可以构造以下断言,每当反推作动器被连接上且有某个飞行状态指示器为“true”时触发。当设定的断言被违反时,它会被突出显示为红色而且也会生成触发这个断言的测试向量。除了 Simulink 中提供的断言模块,Simulink Design Verifier 还提供了其他模块用来定义各种约束,进行模型分析,使您能够在运行仿真前全面分析模型行为并找出设计缺陷。

下一页: 根据需求对设计进行验证

试用 Simulink Design Verifier

获取试用版软件