模型检测最主要的瓶颈是状态空间的爆炸,这就导致早期的模型检测主要用于小型系统的验证。为解决这个问题,偏序约简、有序二叉决策图、抽象等方法被提出。在上述方法中,抽象技术是重要的方法之一。抽象技术是对大型软件系统进行验证的一种有效方法,但其中一个重大的障碍就是对系统的抽象会引入具体系统中本不存在的行为,即可能会引入虚假反例。因此,需要根据反例对抽象模型进行精化,本文的主要研究内容如下:(1)采用动态的抽象精化过程,通过对抽象模型进行精化来消除虚假反例。传统的反例引导的抽象精化方法通过改变可见变量集来分割失效状态,造成其它非失效状态也受影响。本文给出了一种新的划分失效状态的方法:增加布尔变量法。该办法的优点是在抽象精化时,只对失效状态进行重新分割,其他非失效状态不受影响。本文还给出一种新的寻找失效状态的方法,该方法只根据抽象状态的前驱和后继状态来判定其是否为失效状态。对于含有无穷循环的反例,此方法可以避免循环展开时的多项式时间问题。同时,给出并行计算失效状态的方法,快速定位失效状态。最后,综合以上方法,给出了一个反例引导的抽象精化框架。(2)采用静态的抽象精化过程,不对抽象模型进行精化,而是借用一系列精细程度不同的抽象模型和启发式算法来消除虚假反例。本章给出一种静态抽象精化方法,直接对反例进行精化,以判定其是否为虚假反例。该方法将一系列抽象模型作为输入,采用启发式算法,来验证系统的安全属性。从原始模型中提取启发式信息,使用启发式搜索算法,模型检测器可以避免搜索整个状态空间,大大减少空间和时间开销。(3)给出了一种基于权重大小来选择虚假反例的方法。传统的反例引导的抽象精化方法没有考虑到反例的权重。不同的反例路径对抽象精化的影响不同,如果一个反例路径中含有高权重抽象状态,那么该反例的重要性超过其他反例。本文基于此,给出了关键反例的概念,然后借鉴图论中对节点权重的计算方法并将其与抽象技术相结合,重新分析并给出了关键反例识别算法,提高了寻找反例和反例精化的效率。论文从三个方面对反例引导的抽象精化进行优化。第一方面采用动态的精化方法,通过对抽象模型精化来消除虚假反例。第二方面,采用静态的精化方法,不对抽象模型进行精化,而是通过预构建的一系列抽象模型来消除虚假反例。第三方面着眼于寻找权重更大的反例,以提高模型检测效率。第一、二方面讲的是如何从动态静态两种角度来消除虚假反例。第三方面讲的是如何高效地选择虚假反例。