模型检测是一种形式化验证方法,目前已经得到了快速的发展和广泛的应用。模型检测的一个基本问题是状态爆炸,对于这个问题,当前存在很多的解决方法,其中反例引导的抽象精化算法应用较为广泛。反例引导抽象算法虽然在一定程度上能有效缓解状态爆炸问题,但是仍然存在以下两点不足:一是很多类型的错误,例如有关功能正确性的漏洞,如果不通过执行程序是很难检测出来的;二是抽象技术在构建系统模型时总是认为所有的分支都是可达的,遇到反例时才通过精化来消除虚假的反例。而动态执行可以有效避免不必要的细化。基于此,引入本算法——基于反例引导的抽象动态执行精化算法。本算法在反例引导的抽象精化算法基础上加入了动态执行,在构建系统的抽象模型时,能依据程序中的分支节点类型在抽象方法和动态执行方法之间自动切换。本算法将程序中所有的分支节点依据分支条件的确定性划分为确定性分支节点和非确定性分支节点。构造模型的过程中,遇到确定性分支节点时,通过动态执行来计算分支节点的唯一确定后继;遇到非确定性分支时,进行抽象检测,展开所有的分支后继。特别的是,为了高效的利用动态执行的优势,本算法在模型检测前将程序分为确定性程序和非确定性程序两类,对于确定性程序无需通过构建模型来检测,可直接通过动态执行来检测系统的正确性。CPAChecker是一个可靠软件模型检测工具,包括了谓词检测、精确值分析等多种检测方法。谓词检测方法中使用了反例引导的抽象精化算法,其中的抽象技术使用应用广泛的谓词抽象。本算法以CPAChecker的谓词检测方法基础上实现。抽象检测技术可以有效控制系统模型的规模,而动态执行的加入一方面能减少抽象检测方法导致的误判,另一方面能引导系统构建出更加准确的模型,避免不必要的细化。通过实验数据分析,本算法使传统的反例引导谓词抽象精化算法在效率和准确率上都得到了很大的提高。