OneSpin在几年前宣布了一个Quantify MDV产品。有了它，他们定义了许多不同的覆盖方面——可以用他们的正式技术验证的事情。现在他们用一个新版本加强了这个产品。这个版本还包含了另一个覆盖概念。

旧的覆盖概念侧重于设计本身和验证中使用的刺激的质量。它将检查像死代码和过度约束这样的事情，前者反映了可能的代码问题，后者表明现有测试可能无法覆盖合法的情况。我在我的原文中讨论了这些元素报道工具的。

最近，他们在如何称呼这些支票的问题上有点纠结。你可能认为它们只是简单的“设计”检查，除了一些限制性的部分。关于模拟覆盖率，他们将其称为“模拟”覆盖率，但这并不能真正解决问题。他们停留在“可达性”上，因为像死代码或冗余代码这样的东西表明设计元素可能是可达的，也可能是不可达的，而且约束还涉及到测试是否可以到达某些失败。这不是一个完美的命名法，但是，如果没有完美的东西，这就是他们决定的。

为什么还要担心呢?好吧，他们需要将所有这些覆盖方面与他们添加的新内容区分开来。这个新的测试将测试设计中的断言和检查器的完整性。断言的设计目的是在正式验证期间捕捉问题，但也有可能编写无效的断言。从另一种角度来看，如果断言很差或不完整，那么可能存在断言永远无法观察到的代码失败。

所以他们称之为“观察覆盖”。他们使用一种形式的“突变”分析来测试它:做一个代码更改，看看断言是否接受它。如果不是，则断言中可能存在漏洞。

这似乎是一个较新的概念，并且它没有被UCIS覆盖标准所理解;他们正在讨论这个问题。

您可以在他们的网站上获得他们最新Quantify发布的更完整的图片公告．

• 
• 
• 
• 
•