李雅，黄少滨，李艳梅，迟荣华，郎大鹏

(哈尔滨工程大学 计算机科学与技术学院，黑龙江 哈尔滨 150001)



基于遗传算法的反例理解

李雅，黄少滨，李艳梅，迟荣华，郎大鹏

(哈尔滨工程大学 计算机科学与技术学院，黑龙江 哈尔滨 150001)

在复杂系统的错误定位过程中，为了寻找合适的证例，提出一种结合模型检测技术的基于遗传算法的反例理解算法。利用遗传算法，针对模型检测中的模型具有初始状态，状态之间有相应的迁移关系等特点，初始化种群、设计适应度函数并进行指向性的变异操作。实验表明该算法能快速有效的获得最近证例，帮助模型检测的反例理解。

模型检测；遗传算法；反例理解；错误定位

模型检测[1]是一种验证有限状态并发系统(模型)是否满足给定规约的方法[1-2]。当验证的模型不满足给定规约时给出反例是模型检测的一个显著特点。反例是证明模型违反给定规约的执行轨迹。调试者可以通过分析反例，理解错误产生的原因，对系统或模型进行修正。然而反例并没有明确指出模型错误的原因，需要调试者根据自己的经验定位错误，这需要花费大量的时间才有可能找到真正的错误，因此使用自动化的方法从反例中获取有用的信息，帮助用户定位错误，是目前的研究热点。许多研究人员致力于研究错误定位的算法，提出了许多经典的算法，如基于路径的语法级最弱前置条件的辅助算法[3]，利用克雷格插值的证明方法[4]，基于因果关系模型的方法[2,5]，基于可满足性的方法[6-7]，以及基于证例和反例差异的方法[8-11]。……