随着硬件和软件系统复杂性的不断增加，错误的出现概率也将越来越高．这些错误可能给我们带来物质和时间的损失，甚至灾难．形式化验证的意义在于它能帮助我们发现一些隐蔽的系统错误，有助于增加工程师对系统可靠性的信心．形式化验证是创建一个系统的数学模型，使用一个语言来准确无二意性地描述属性需求，并使用一种证明方法来验证模型是否满足属性需求．当这个证明能够充分的机械化运行，我们称为自动化验证． 经过25年的发展，模型检测(Model Checking)已经成为广泛应用的自动化验证技术之一．其基本思想是使用有穷状态模型M来描述系统行为，使用时态逻辑公式，来描述属性规约，这样，“系统是否满足属性规约?”转化为数学问题“M是否是逻辑公式f的一个模型?，即M｜=f?”． 模型检测通常需要遍历可达状态空间来完成验证任务．对于并发系统，状态个数往往随并发分量的增加而指数增长，由此带来所谓的状态爆炸问题．为了有效应用模型检测的方法，需要减少或者压缩状态空间。上世纪90年代初，McMillan等提出的符号化模型检测技术使得这一方法向工业应用迈出了关键的一步．他们使用BDD表示状态集合和迁移关系，模型检测的不动点运算能够直接转化为BDD的运算．这种方法的关键之处在于BDD紧凑表示的变量顺序，然而这种顺序不容易寻找而且不一定存在．因而即使采用符号化表示技术，在一些大型工业应用中，模型检测仍然受限于状态爆炸问题．因此，相关的约简技术成为热门的研究课题，抽象(abstraction)则是其中最为普遍和重要的技术之一． 抽象是将系统描述映射成一个较小的有穷状态模型，同时保证验证结果的特定要求．验证较小的抽象模型自然比原始模型更为高效．然而，抽象技术的主要困难是如何构建恰当的抽象模型，因为过于粗糙的抽象会令验证失败而无法得出结论，过于精确的抽象会令模型过大而无法在有限的时间和空间内完成验证．理想的抽象模型满足(1)有效性：能够得出验证结果；(2)极小性：不存在更小的有效抽象模型．本论文着重研究如何在模型检测中使用抽象及其极小化理论和方法． 本论文关注了近年来最为成功之一的谓词抽象技术．谓词抽象是选取一个有穷谓词集合P，将系统映射在P上来生成有穷状态模型．我们提出了Petri网的自动化谓词抽象技术，即如何选取谓词集合并迭代产生新谓词，以此剔除虚假反例，逐步精化(refinement)，直至验证结束或者资源用尽．同时我们创新地提出变迁失败层次(transition failure level)方法来极小化新谓词，以此获得简洁紧凑的谓词集合，提高模型生成速度．在另一方面，我们也注意到，在每一个迭代阶段，通常需要重新构建新的谓词抽象模型，因而重复需要指数次地(相对于谓词个数)调用定理证明器．为此，我们提出一种路径分裂的局部精化(refinement)方法，直接剔除虚假反例，不需要重新构建模型，也不引入新的谓词．这样带来的另外一个好处就是模型大小随反例长度线性增长而不是随谓词个数指数增长． 近年来，有界模型检测(Bounded Model Checking，BMC)成为SAT技术在模型检测中的成功应用之一．BMC的基本原理是将模型的有界(假设为к)路径和属性规约转化为命题公式F，使得F是可满足的当且仅当模型存在长度为к的反例．近十年来，SAT技术的突飞猛进，产生了大量的高效SAT工具，使得这种反例查找方法切实可行．然而，BMC通常只适用查找短浅(к较小)的反例，因为随着深度增加(к增大)，公式F过大从而导致SAT工具无法在有限时间内判断其可满足性．抽象技术能够增加BMC的反例查找深度． 本论文提出了变量抽象在命题逻辑中的一般化概念，称为近似(approximation)． 本论文中，我们创新提出了近似有界模型检测(ABMC)技术，基本原理是选取一个系统变量子集V，将模型的有界(假设为к)路径和属性规约转化为上近似公式F°和下近似公式Fu．若F°不可满足，则不存在长度为к的反例，因而需要增加查找深度尼．若Fu可满足，则存在长度为к的反例，因而输出反例结束验证．否则，选取新的变量子集V，直至近似公式满足以上两种条件之一．由于近似公式通常比原始公式小得多(变量少)，当查找深度к较大时，判断相应近似公式是否可满足更为容易，从而潜在地增加了反例查找深度．而且基于我们方法得出的反例包含较少变量，因而更有利于用户分析反例产生的原因．