形式化验证简介

目前保证实时操作系统正确性的方法主要有测试、仿真和形式化方法。测试和仿真是工业界通常采用的方法，简单易行，但是必须要等到系统的原型实现后才能展开，并且只能检测出某个错误是否出现在系统中，却不能保证系统中没有错误，这使得测试和仿真不能从根本上保证实时操作系统的正确性。相反，形式化方法是一种基于数学理论的严格方法，使用数学符号抽象系统模型和系统期望性质，通过推理或图形搜索的方式验证系统的形式化模型是否满足规范。形式化方法能够避免非形式化方法产生的模糊性、二义性以及不一致性等，进而能够比较深入的检测到系统中可能存在的细微的漏洞。另外，从系统设计阶段开始就能够应用形式化方法，而不用等到系统原型实现后再进行。

形式化验证主要由模型检测和定理证明两种方法组成。模型检测基于模型理论，以穷尽搜索系统状态空间的方式判断模型是否满足性质。为了确保搜索的终止性，模型的状态空间通常会被限制为有穷。在模型检测中，可以使用上述各种形式化规范语言作为建模语言，而一般使用时序逻辑作为性质描述语言。模型检测是一种自动化的验证方法，能够在模型不满足性质时。给出反例，便于定位和修改模型。然而，它受制于状态空间爆炸问题。针对该问题，各种改进的模型检测方法被提出。 1987 年 McMillan 使用简化有序二叉决策图(Reduced Ordered Binary Decision Diagrams， ROBDD) 隐含地描述状态集合，从而提出了符号模型检测方法。随后，基于高效的 SAT 求解器，提出了限界模型检测方法。此外，还存在许多其它压缩状态空间方法，例如偏序模型检测、组合模型检测和抽象模型检测等，从而扩大了模型检测的适用范围。典型的模型检测工具有： SPIN、 SMV、 NuSMV等。

定理证明建立在证明论的基础上，将系统的模型和期望性质表示成公理系统中的定理，通过证明该定理在该公理系统中是有效的来证明模型满足性质。使用定理证明方法时，通常需要先构建某个逻辑下的公理系统。定理证明具有通用性，既适用于有穷状态系统，也适用于无穷状态系统。同时，证明的细节使得用户能更深层次地了解系统。但是，定理证明往往需要人的辅助才能进行。随着人工智能的发展，产生了机械化定理证明，在证明定理时能够使用自动化的工具完全或部分地替代人工证明。机械化定理证明依据自动化程度和底层逻辑表达能力的不同，可以粗略地分为自动定理证明和交互定理证明（即半自动定理证明）。常用的定理证明器包括有： PVS、 Isabllea/HOL、 Coq和 ACL2等。