形式化验证就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中的不一致性、模糊性、不完备性等错误。形式化验证的主要技术包括模型验证和定理证明。

模型检验

1.概述

模型检验是一种基于有限模型并检验该模型的期望特性的一种技术。粗略地讲，检验就是状态空间的蛮力搜索，模型的有限性确保了搜索可以终止。

模型检验有两种主要方法。其一是时态模型检验，该方法中规格以时态逻辑形式表述，系统模拟为有限状态迁移系统。有效的搜索过程用来检验给定的有限状态迁移系统是否是规格的一个模型。另一种方法中，规格以自动机方式给出，系统也模拟为一个自动机。系统的自动机模型和规格比较，以确定其行为是否与规格的自动机模型一致。一致性概念已进行了广泛的研究，包括：语言包含、细化有序、观测等价等。

不同于定理证明，模型检验是完全自动且高效的。模型检验可用于系统部分规格，因此可用于未完全规格的系统。

模型检验的主要局限性在于状态组合爆炸问题。有序布尔决策图OBDD是表述状态迁移系统的高效率方法，使得较大规模系统的验证成为可能。其他可能改善状态组合复杂性的途径有利用偏序信息、局部简化、语义最小、消除不必要状态等几种。

目前，模型检验预计可以处理100~200 个状态变量的系统。模型检验已用来检验状态数目可达 10的120次的系统，并且通过采用适当的抽象技术就可以处理本质上无限状态的系统。模型检验的技术挑战在于设计可以处理大型搜索空间的算法和数据结构。

2.应用

模型检验已在硬件电路、协议的验证、软件系统规格与分析中得到成功的应用。

（1）硬件电路

贝尔实验室对其高级数据链路控制器在FormalCheck下进行了功能验证，6个性能进行了规格，其中5个验证无误，另外一个失败，从而进一步发现了一个影响信道流量的Bug。LOTOS用于PowerPC中的微处理器，对其中4个基本功能特性进行了验证。基于CCS语言对楼宇抗震分布式主动结构控制系统设计进行了规格，所生成的系统模型有2.12×1019数目的状态，经过自动分析发现了影响主动控制效果的计时器设置错误。

（2）协议的验证

基于SMV输入语言建立了IEEE Futurebus+896.1－1991标准下cache一致协议的精确模型，通过SMV验证了迁移系统模型满足cache一致性规格。从中发现了先前并未找到和潜在的协议设计中的错误。这项工作是第一次从IEEE标准中发现错误。Murphi有限状态验证系统对IEEE标准1596－1992下cache一致协议进行了验证，发现了变量、逻辑等方面的错误；Philips公司音响设备的控制协议通过HyTech得到了完全自动验证，这是一个具有离散和连续特征的混杂系统验证问题。

（3）软件系统规格与分析

形式化模拟和验证用于AT&T公司的通信软件开发，总共对7500条SDL源代码进行了验证，从中发现112个错误，约55％的初始设计需求在逻辑上不一致。

3.模型检验器

模型检验的工业应用离不开模型检验器的支持。工业应用部门可以选取现有的、也

（1）时态逻辑模型检验器
时态逻辑模型检验器中，EMC和CESAR是最早的两个；SMV中使用了OBDD；Spin中采用偏序关系简化来改善状态组合复杂性；Murphi和UV基于Unity编程语言；Concurrency Workbench验证由mμ演算公式表述特性的CCS；SVE、FORMAT和CV侧重于硬件验证；HyTech用于混杂系统；Kronos用于实时系统。

（2）行为一致检验器
行为一致检验器中，Cospan/Formal Check基于自动机间的包含；FDR检验CSP程序的细化；Concurrency Workbench检验CCP程序细化。

（3）复合检验器
复合检验器中，HSIS复合模型检验和语言包含；Step复合模型检验和演绎方法；VIS复合模型检验和逻辑综合；PVS定理证明器中有用于模态mμ演算的模型检验器；METAFrame是支持整个软件开发过程模型检验的环境。

定理证明

1.概述

定理证明是系统及其特性均以某种数学逻辑公式表示的技术。逻辑由一具有公理和推理规则的形式化系统给出。定理证明实质上是从系统公理中寻找特性证明的过程。证明采用公理或者规则，且可能推演出定义和引理。不同于模型检验，定理证明可以处理无限状态空间问题。定理证明系统可粗略地分为自动的和交互的两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功；交互式定理证明系统则更适合于系统的形式化开发和机械形式化。同样地定理证明的实施也是需要定理证明器的支持。

现有的定理证明器包括：用户导引自动推演工具、证明检验器和复合证明器。用户导引自动推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL，这些工具由引理或者定义序列导引，每一个定理采用已建立的推演、引理驱动重写和简化启发式来自动证明；证明检验器有Coq、HOL、LEGO、LCF和Nuprl；复合证明器Analytica中将定理证明和符号代数系统Mathematica复合，PVS和Step将决策过程模型检验和交互式证明复合在一体。

2.应用

定理证明在硬件和软件设计的安全特性验证中得到了应用。基于符号代数运算的自动定理证明用于证明Pentium中SRT算法的正确性，检查出了一个由故障商数字选择表引起的错误；PowerPC和System/390中寄存器传输级、门级、晶体管级的硬件设计模拟为布尔状态迁移函数，基于OBDD的算法用来检验不同设计级上状态迁移函数的等价性；Nqthm用于Motorola 68020微处理器的规格该规格，进而用来证明不同来源的二进制机器码的正确性。

ACL2用于AMD5K86的浮点除微代码的规格和机械证明，ACL2还用来检验浮点方根微的正确性，发现了其中的Bug，并对修改后的微代码进行了正确性机械证明；ACL2用于Motorola复数算术处理器CSP的完全规格，同时对CSP的几个算法进行了验证；PVS用于航空电子微处理器AAMP5的规格和验证，对209条AAMP5指令中的108条进行了规格，验证了11个有代表性的微代码。