计算机系统形式化验证中的模型检测方法综述

　　1 形式化方法概述
　　形式化方法是用数学和逻辑的方法来描述和验证系统设计是否满足需求。它将系统属性和系统行为定义在抽象层次上，以形式化的规范语言去描述系统。形式化的描述语言有多种，如一阶逻辑，Z语言，时序逻辑等。采用形式化方法可以有效提高系统的安全性、一致性和正确性，帮助分析复杂系统并且及早发现错误。形式化验证是保证系统正确性的重要方法，主要包括以数学、逻辑推理为基础的演绎验证(deductive verification)和以穷举状态为基础的模型检测(model checking)。演绎验证是基于人工数学来证明系统模型的正确性。它利用逻辑公式来描述系统，通过定理或证明规则来证明系统的某些性质。演绎验证既可以处理有限状态系统，又可以解决无限状态问题。但是演绎验证的过程一般为定理证明器辅助，人工参与，无法做到完全自动化，推导过程复杂，工作量大，效率低，不能适用于大型的复杂系统，因而适用范围较窄。常见的演绎验证工具有HOL，ACL2，PVS和TLV等。模型检测主要应用于验证并发的状态转换系统，通过遍历系统的状态空间，对有限状态系统进行全自动验证，快速高效地验证出系统是否满足其设计期望。下面将主要介绍模型检测方法的发展历史和研究现状，以及当前面临的挑战和未来发展方向等问题。
　　2 模型检测及相关技术
　　模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式。检测系统模型是否满足时态逻辑公式，如果满足则返回是，不满足则返回否及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear TemporalLogic)和计算树逻辑CTL(Computation Tree Logic)。
　　2.1 线性时态逻辑
　　对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：(与)， (或)，|(非)，(逻辑包含)，(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-time)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M 中是否存在从某个状态出发的并满足LTL公式| 的路径，如果所有路径都满足LTL公式 则不存在有路径满足|。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。
　　2.2 计算树逻辑
　　计算树即为通过将迁移系统M 某一状态作为根，将M 用树形结构展开表示出来，CTL使用路径量词(包括：A(All)，E(Exist))和时态算子(包括F，G，X，U)对计算树属性进行形式化的描述，表示出系统的状态变化以及状态的分枝情况。LTL的时间定义是与路径相关的，每个时刻只有唯一的一个后继状态。LTL可用于有重点的选择感兴趣的路径分析，并且LTL可以表达公平概念而CTL不能。但是对于一些复杂属性，如每个计算总是可能返回到初始状态，LTL将无法描述，但是CTL可以。CTL的时间定义是与状态相关的，每个状态都有多个可能的后继状态，从一个给定的状态量化分离出路径，能够断言行为的存在。CTL可以用路径量词E，而LTL不可以;CTL公式使用路径量词A时与LTL公式表达内容可以相同。LTL和CTL各有优势，Emerson等人提出扩展的时间逻辑CTL，提供了一种统一的框架，包含了LTL和CTL，但是可满足性判定代价较高。
　　2.3 模型检测工具
　　模型检测因其自动化、高效等特点得到广泛应用，各类模型检测工具也层出不穷。以下是几类典型的模型检测工具。SPIN是1980年美国贝尔实验室开发的模型检测工具，主要关心系统进程间的交互问题。它以promela为建模语言，以LTL为系统属性的逻辑描述语言，支持on-the-fly技术，可以根据用户的需要生成系统的部分状态，而无需构建完整的状态迁移图。SPIN验证器无法验证实时系统。NuSMV是1987年由McMillan提出的开源的符号模型检测工具。它可以工作于批处理模式，也可以工作于交互模式。NuSMV采用扩展的SMV语言描述系统，并用CTL和LTL描述需求。NuSMV结合了以可满足性(SAT)为基础的模型检测和以二叉决策树BDD(Binary Decision Diagram)为基础的模型检测。它具有健壮性，以模块形式构建，不同模块间无依赖关系，代码易修改。提供了同步模型和异步模型的分区方法，可以结合可达性分析，验证不变性质。NuSMV非常灵活，使用者可以控制并且可以改变其系统模块的执行顺序，并且可以检查和修改系统的内部参数来调整验证过程。普通的有限状态转换图无法模拟动态变化的物理环境，于是出现了由时间自动机与有着一系列变量的状态转换图结合而成的新模型。UPPAAL就是基于这种模型的成熟的实时系统验证工具。UPPAAL是1995年由Aallorg大学和Uppsala大学共同提出，具有可视化图形编辑器。它基于时间自动机并对其进行扩展，引入了坚定位置、初始化程序、紧迫位置和紧迫管道等概念，有助于对真实系统进行建模，并能够有效减少系统内存占用。它被用于检测不变量和可达性属性，尤其是检测时间自动机的控制节点某些组合以及变量约束是否满足初始配置。CPN-Tool是由Aarhut大学开发的工具，用于有色petri网CPN(Colored Petri Net)的构造和分析。有色petri网是用于对系统进行建模并验证其并发、通信和同步的语言，是一种描述离散事件的图形化建模语言。它基于meta-language，并有强大的可扩展性。它能够通过仿真分析系统的行为，通过模型检测验证系统属性。对于状态爆炸问题，CPN-Tool有很多方法来减少状态数量，Christensen等人使用全局时钟和时间戳作为标记，通过状态等价关系化简状态空间，将无限状态转化为有限状态。
　　2.4 状态爆炸问题
　　模型检测使用状态空间检索来进行系统验证。状态空间检索的主要缺点就是状态空间随着进程数量增CTL使用路径量词(包括：A(All)，E(Exist))和时态算子(包括F，G，X，U)对计算树属性进行形式化的描述，表示出系统的状态变化以及状态的分枝情况。
　　CTL和LTL都有强大的表达能力。LTL的时间定义是与路径相关的，每个时刻只有唯一的一个后继状态。LTL可用于有重点的选择感兴趣的路径分析，并且LTL可以表达公平概念而CTL不能。但是对于一些复杂属性，如每个计算总是可能返回到初始状态，LTL将无法描述，但是CTL可以。CTL的时间定义是与状态相关的，每个状态都有多个可能的后继状态，从一个给定的状态量化分离出路径，能够断言行为的存在。CTL可以用路径量词E，而LTL不可以;CTL公式使用路径量词A时与LTL公式表达内容可以相同。LTL和CTL各有优势，Emerson等人提出扩展的时间逻辑CTL，提供了一种统一的框架，包含了LTL和CTL，但是可满足性判定代价较高。
　　3 模型检测的新进展
　　尽管模型检测验证能力在不断增强，可是对于复杂系统的验证仍然面临许多挑战。验证混成系统时，由于其状态空间庞大，对于一些基础问题的验证，具有不可判定性。验证系统的访问控制策略时，一条策略可能包含大量规则，如何对策略建模成为难点。验证多智能系统MAS(Multi-Agent System)时，由于MAS出现的目的就是用多个模块来解决单一模块无法解决的复杂问题，因此MAS的使用环境一般较为复杂，行为多样且具有随机性，验证难度较大。本文针对上述难题，提出一些解决方法如下。验证混合自动机。Krishna等人用混合自动机模型化物联网系统，并且用LTL模型检测进行验证。在使用LTL模型检测混合自动机时，由于LTL具有不可判定性，引入互模拟的概念，并表明一个有限互模拟的存在意味着使得LTL模型检测问题的可判定。验证访问控制安全策略。Maarabani等人将组织间模型O2O(Organization to Organization model)与LTL模型相结合，来验证互操作访问控制安全策略。将每一个O2O策略分别用两个LTL公式表示，进行验证。Hwang，Tao等人定义了一个新的工具ACPT(Access Control Policy Testing)，将策略制定者的安全需求，转化成可执行的策略，并根据需要对访问控制策略进行动态和静态验证验证MAS。Meski等人用基于SAT的限界模型检测和基于BDD的限界模型检测分别验证多智能系统MAS，并对两种验证方法的时间和内存耗费方面等进行比较。由于目前对MAS的验证技术不支持主流验证工具，且输入形式单一，Hunter等人提出扩展验证框架可以支持多种输入，并且提供翻译器将输入翻译为多个主流验证工具的输入语言，利用现有的验证工具对MAS进行验证。由于MAS的使用环境相对复杂，其行为具有随机性，Song针对MAS行为具有随意性的难题，提出一种概率建模语言对MAS的进行描述，并提出相应的模型检测框架。
　　4 结束语
　　形式化验证方法已经被广泛的研究，各种描述语言与验证工具层出不穷。相对于演绎验证，模型检测因其全自动并可以提供有数学基础的反例等特点，适用范围更广，可用于验证软件、硬件和协议系统等多个领域。利用模型检测时需控制好状态数量，进行存储压缩或者使用必要的路径压缩、状态缩减算法非常关键。同时前期对于保护目标的选取也非常关键，选出关键资产来保护可以大大提高后期的描述与验证效率。本文工作可为模型检测方法的研究提供借鉴和参考意义。