摘要: 如今，数字系统的形式化验证主要有两种形式：状态检测（如模型检测）和演绎推理（如定理证明），且各有优缺点。模型检测能够自动验证有限状态系统的时序性质，并且在性质不成立时很容易生成反例，这对改正系统错误以及声明错误来说是非常重要的，而它的缺点就是容易产生状态爆炸的问题，从而影响了可验证问题的规模。定理证明则是将待验证的性质表述成数学逻辑描述的定理，然后用定理证明器对其进行证明，这一方法基于一阶和高阶逻辑，可以对无限状态的系统进行验证，但是当性质不成立时，定理证明器没有相应的反馈，有反馈的也需要专业的人士才能通过反馈找出问题所在，因此，在改正和调试系统方面，定理证明就不如模型检测有优势。因此，为了将这两种方法结合起来，既克服各自的缺点，又可以保持各自的优势，有人提出了在模型检测之上加入一个演绎推理的层级的方法，也有人提出将模型检测嵌入到演绎推理的过程当中。本文的研究是基于后者的，而研究的目的就是要得到一个最好的模型检测工具和定理证明器。在本文中，我们给出了一个在高阶逻辑（HOL）定理证明器中定义抽象状态检测所必须的基础结构。这个基础结构是以在高阶逻辑中嵌入多路判定图（MDG）理论为基础的。用多路判定图代替二叉判定图表（BDD）来表示和操作一阶逻辑公式的一个子集，可以更好的定义嵌入定理证明器当中的模型检测。同时，对于多路判定图本身来说，我们用一个抽象数据类型的单个变量来表示多路判定图中的一个值，而不是用布尔向量来表示，这样可以使系统的表示更加紧凑。用多路判定图代替二叉判定图表，使得在定理证明器中的抽象层级上，我们可以对系统进行状态检测。另外，多路判定图这一结构还提高了整个证明的自动性和可验证问题的规模，而这些在我们给出的实验中也很好的表现了出来。在今后的工作当中，我们会进一步的考虑工具的完备性，并争取在商用的模型检测工具中运用我们的技术，我们也坚信这项技术能有效的改善模型检测工具的效率，使其在现实生活中发挥更大的作用。