基于克雷格插值的反例理解方法

摘要：

针对错误原因提取效率低的问题,提出一种利用克雷格插值对模型检测器产生的反例进行自动理解的方法.该方法首先从反例失效状态出发推导出其最弱前置条件,然后对初始状态与反例最弱前置条件进行不一致分析,能在线性时间内提取克雷格插值作为反例失效原因,产生的插值能直接用于定位错误事件.实验结果表明,基于克雷格插值的反例理解方法能显著提高反例理解速度,提高软件的调试效率,从而提升软件的可靠性和质量.

关键词：模型检测、反例、反例理解、最弱前置条件、克雷格插值

所属期刊栏目：51

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金60873038;国家科技支撑计划项目2009BAH42B02

在线出版日期：2013-03-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：94-100