Error Explanation with Distance Metrics
Error Explanation with Distance Metrics
复制标题
DOI：
10.1007/978-3-540-24730-2_8
复制
发表时间：
2004-03
期刊：
影响因子：
--
通讯作者：
Alex Groce
中科院分区：
文献类型：
--
作者：
Alex Groce
如果系统不满足规范，模型检查器通常会自动生成反例跟踪，显示不良行为的特定实例。不幸的是，发现反例之后的重要步骤通常不是自动化的。用户必须首先确定反例是否显示了真正的错误行为，或者是不正确的规范或抽象的产物。如果错误确实存在，那么充分理解错误以隔离和修改系统的故障方面仍然是一项艰巨的任务。本文描述了一种帮助用户理解和隔离 ANSI C 程序中的错误的自动化方法。该方法基于程序执行的距离度量。实验结果表明，模型检查引擎的强大功能可用于帮助理解错误并隔离源代码的错误部分。
In the event that a system does not satisfy a specification, a model checker will typically automatically produce a counterexample trace that shows a particular instance of the undesirable behavior. Unfortunately, the important steps that follow the discovery of a counterexample are generally not automated. The user must first decide if the counterexample shows genuinely erroneous behavior or is an artifact of improper specification or abstraction. In the event that the error is real, there remains the difficult task of understanding the error well enough to isolate and modify the faulty aspects of the system. This paper describes an automated approach for assisting users in understanding and isolating errors in ANSI C programs. The approach is based on distance metrics for program executions. Experimental results show that the power of the model checking engine can be used to provide assistance in understanding errors and to isolate faulty portions of the source code.