Main Content

本页采用了机器翻译。点击此处可查看英文原文。

证明大型模型中的属性

属性证明使用与设计错误检测和测试生成相同的底层技术，并且受到相同的性能限制。然而，与设计错误检测或测试生成不同，您通常无法在不损害结果有效性的情况下简化问题。

您可以快速证明不受模型动态影响的简单证明目标。然而，彻底的证明需要Simulink® Design Verifier™搜索模型的所有可达配置 — — 即使是经过长时间延迟才能达到的配置。完全搜索模型所需的计算时间和内存通常会使详尽的证明变得不切实际。

有两种技术可以用来提高大型模型中属性证明的性能：

在设计模型时查找属性违规

Simulink Design Verifier 软件提供了一种策略，可以快速识别更大、更复杂的模型中的属性违规行为。在设计模型时，使用此策略分析模型，以便您可以在完成设计之前修复任何属性违规。

要识别模型的属性违规，请在配置参数对话框的 Design Verifier > Property Proving窗格中将 策略 参数的值指定为 FindViolation 。当您使用此策略时，最大违规步数 参数将变为活动，以便您可以指定搜索中时间步数的上限。

在分析过程中，软件仅搜索指定时间步长内的属性违规。通过首先识别和修复属性违规，您可以提高使用 Prove 策略的属性证明分析的性能。

如果没有检测到违规，则任何时间步长少于指定限制的输入序列都不可能违反该属性。但是，您无法证明该属性是正确的，因为在比指定的限制更多的时间步内可能会存在反例。

结合证明性质和查找证明违规

使用以下技术来证明大型模型中的属性。该技术结合了证明和搜索违规行为：

  1. 在 Design Verifier > Property Proving窗格上，将 策略 参数设置为 Prove 。

  2. 在 Design Verifier窗格上，对 最大分析时间 参数使用相对较短的值，例如 5-10 分钟。如果存在简单的反例——或者您的属性不依赖于模型动态——则分析应该在那段时间内完成。

  3. 将 策略 参数更改为 FindViolation，并为 最大违规步数 参数选择一个较小的边界，例如 4、5 或 6 。如果您的属性有简单的反例，软件应该会发现它们。

  4. 如果您没有发现任何违反较小界限的情况，请增加界限并寻找更长的反例。

    1. 分几次增加边界，并观察处理时间和内存消耗。系统资源可能会限制可搜索的违规长度。

    2. 此外，请考虑模型的动态以及任意一对配置之间转换所需的时间步数。如果选择的界限太大，违规搜索可能比无界证明更复杂。

  5. 如果您可以运行具有相对较大界限的违规搜索（例如 30-50 个时间步），请切换回 Prove 策略，并使用更长的时间限制，例如几个小时。