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

Understanding Counterexamples Based on Craig Interpolation

作　　者：黄宏涛 黄少滨[1] 陈志远[1] 张涛[1] 

机构地区：[1]i哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《吉林大学学报（理学版）》2013年第1期94-100,共7页Journal of Jilin University:Science Edition

基　　金：国家自然科学基金(批准号:60873038);国家科技支撑计划项目(批准号:2009BAH42B02)

摘　　要：针对错误原因提取效率低的问题,提出一种利用克雷格插值对模型检测器产生的反例进行自动理解的方法.该方法首先从反例失效状态出发推导出其最弱前置条件,然后对初始状态与反例最弱前置条件进行不一致分析,能在线性时间内提取克雷格插值作为反例失效原因,产生的插值能直接用于定位错误事件.实验结果表明,基于克雷格插值的反例理解方法能显著提高反例理解速度,提高软件的调试效率,从而提升软件的可靠性和质量.An interpolation based method was proposed to automatically understand counterexamples produced by model checker. By this method the weakest pre-condition of a counterexample was first derived from its failure state, and then inconsistent analysis was performed on the initial state and the weakest pre-condition of the counterexample. Craig interpolations which can be extracted in linear time are the causes of model failure; these causes can be mapped to corresponding events directly. Experimental results show that our method improves the efficiency of understanding counterexamples remarkably, which can reduce the burden of software debugging workers and promote reliability and quality improvement of software.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]