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

Understanding Counterexamples Based on Craig Interpolation

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

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.