关键词：
模型检测
错误定位
最弱前置条件
可满足性求解
支持向量机
摘要：
信息技术的飞速发展使得计算机软硬件系统的应用领域不断扩大,其规模和复杂程度也日益提升,软硬件系统的正确性和可靠性问题日益严峻,同时带来了许多不可估量的风险。要保证软硬件系统的正确性和可靠性,需要通过大量的测试和调试工作,然而软硬件的测试和调试是一项成本昂贵且需要许多人工参与的工作。因此提出高效地自动地针对大规模软硬件系统的错误定位方法具有重要的理论和应用意义。形式化的方法能够在早期发现系统的不一致、歧义和错误等问题,是一种有效的提高软硬件系统正确性和可靠性的方法。模型检测是一种比较常见的系统形式化验证方法。当利用模型检测方法对软硬件系统进行验证时,如果系统模型不满足待验证性质,模型检测器会给出一个反例,表明系统模型存在缺陷或者错误。然而模型检测器只给出了存在错误的现象,并没有指出错误的原因。错误可能存在于性质中,也可能来源于建模过程,再或者是软硬件系统自身的缺陷。同时随着系统规模的日益增大,反例变得越来越长也越来越复杂。因此研究基于模型检测的错误定位具有重要意义。然而模型检测主要用于并发系统的验证,对于顺序变换程序,往往需要基于证明的方法才能够对其进行验证,因此需要基于定理证明的程序错误定位方法。基于此本文开展了以下几个方面的工作。1)针对有界模型检测验证过程中的可满足性问题的求解,提出了利用支持向量机求解可满足性问题的方法。该方法充分利用支持向量机在解决小样本、非线性问题上的优势,针对可满足性问题变量取值的特点,将可满足性问题的求解看作一个二分类问题。首先依据每个可满足性问题的特征搜集训练样本,依照支持向量机的训练算法得出分类器。再对可满足性问题中的变量进行二分类,最终将变量的分类结果用于不完全算法中的初始化赋值,减少求解过程中变量取值的翻转次数;也可以将分类结果用于完全算法中的变量决策过程,降低搜索树的复杂度。2)基于通过对比证反例获取错误位置的方法,针对采用模型检测器验证软硬件系统的特点,利用模型检测器在验证失败时给出的反例,提出了一种基于可满足性求解和反例引导的最近证例求解方法。该方法在有界模型检测器给出反例之后,将待验证系统模型和待验证性质编码成一个证例满足,但反例不满足的SAT实例。将这一可满足实例转换成合取范式的形式,利用类似完全算法DPLL的可满足性问题求解方法和反例中的变量取值信息引导生成的SAT问题的求解过程,最终生成一组该SAT问题的可满足解,也就是证例。为了保证证反例最近,迭代的执行证例求解,最终按照与反例的距离选取最合适的证例与反例进行比较,得到最可能的错误位置。3)针对基于反例引导的错误定位方法对模型检测工具依赖性大和模型检测器生成的SAT实例规模庞大的问题,提出了一种不依赖于具体问题的具有普适性和天然并发性的基于改进遗传算法的反例理解方法。根据模型检测验证方法的模型特点设计规模较小的初始化种群;依据证例需要满足的两个条件,构建多个适应度函数,最大程度的遗传父本的优秀基因;定向性的变异操作,既保证种群的多样性,又避免无效个体的产生,加快算法的收敛速度和提高算法的效率。实验表明基于改进遗传算法的反例理解方法通过引入启发式信息,缩减了系统搜索的状态空间,收敛速度较快,适用性更强应用范围更广。4)针对模型检测技术不能验证顺序变换程序,并且生成的反例规模庞大的问题,利用基于证明的方法,提出了一种基于最弱前置条件的快速错误定位算法。该方法从程序需要满足的断言开始,通过程序语句最弱前置条件的推导规则计算出整个程序需要满足的最弱前置条件,然后为其构造出错误分析图;之后在错误分析图上执行两次简单的标记过程,找到两次标记的冲突节点作为疑点语句,从而完成错误定位。实验表明,相对于其它方法,基于最弱前置条件的错误定位方法能够有效的提高程序错误定位的精度,能够大大减少调试人员的工作量。
欢迎来到三峡大学图书馆！
