Sanity Checks in Formal Verification
Sanity Checks in Formal Verification
复制标题
形式验证中的健全性检查
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
O. Kupferman
中科院分区：
文献类型：
--
作者：
O. Kupferman
时态逻辑模型检测工具的优势之一是，它们能够伴随反例对正确性查询的否定回答，从而满足系统中的规范。另一方面，当对正确性查询的回答是肯定的时，大多数模型检查工具不会提供额外的信息。在过去的几年中，人们越来越意识到怀疑系统的重要性，或者在模型检查成功的情况下也要包含错误的规范。这种怀疑的主要理由是系统或规范的建模中可能存在错误。健全性检查的目标是通过进一步的自动推理来检测此类错误。两个主要的健全检查是真实性和覆盖率。在真空中，目标是检测系统以某种意想不到的琐碎方式满足规范的情况。在覆盖面方面，目标是通过检测在验证过程中不起作用的系统组件来增加规范的详尽程度。对于这两种检查，挑战是正式定义空洞和覆盖，开发检测空洞满意度和低覆盖的算法，并建议返回给用户有用信息的方法。我们综述了现有的关于真空性和覆盖率的工作，并认为，在许多方面，这两种检查本质上是相同的：两者都基于对一些突变输入的重复验证过程。在真空中，突变在规范中，而在覆盖中，突变在系统中。这种观察使我们能够采用在虚无的背景下所做的工作来报道，反之亦然。
One of the advantages of temporal-logic model-checking tools is their ability to accompany a negative answer to the correctness query by a counterexample to the satisfaction of the specification in the system. On the other hand, when the answer to the correctness query is positive, most model-checking tools provide no additional information. In the last few years there has been growing awareness to the importance of suspecting the system or the specification of containing an error also in the case model checking succeeds. The main justification of such suspects are possible errors in the modeling of the system or of the specification. The goal of sanity checks is to detect such errors by further automatic reasoning. Two leading sanity checks are vacuity and coverage. In vacuity, the goal is to detect cases where the system satisfies the specification in some unintended trivial way. In coverage, the goal is to increase the exhaustiveness of the specification by detecting components of the system that do not play a role in verification process. For both checks, the challenge is to define vacuity and coverage formally, develop algorithms for detecting vacuous satisfaction and low coverage, and suggest methods for returning to the user helpful information. We survey existing work on vacuity and coverage and argue that, in many aspects, the two checks are essentially the same: both are based on repeating the verification process on some mutant input. In vacuity, mutations are in the specifications, whereas in coverage, mutations are in the system. This observation enables us to adopt work done in the context of vacuity to coverage, and vise versa.