状态空间进行搜索在实际上是不可行的。这就是所谓的状态爆炸问题。 为了能够有效地应用模型检测方法,需要研究减少和压缩状态空间的方法。 文献上关于这方面的文章很多,其中的很多方法已经实现在不同的模型检测工具 中。以下介绍几种常用方法。 符号模型检测的基本原理是将系统的状态转换关系用逻辑公式表示[18]。在 这方法中,二叉图( Binary Decision Diagram)是用以表示逻辑公式的重要手 段[21],它能较为紧凑地表示状态转换关系,以降低系统模型所需的内存空间 另外,状态转换的计算可以以集合为单位,以提高搜索的效率。符号模型检测为 克服“状态爆炸”问题迈出了关键的一步。 on-the-fly模型检测的基本原理是根据需要展开系统路径所包含的状态, 避免预先生成系统的所有状态[22]。一个系统可以由多个进程组成,并发执行使 得不同进程的动作可以有许多不同的次序。基于对这一问题的认识,我们可以将 某些状态的次序固定,以减少重复验证本质上相同的路径。这种方法称为偏序归 约[23][24]。 由多进程组成的系统中某些进程可能完全类似,并发执行的结果可能产生许 多相同或相似的路径。基于对这一问题的认识,我们可以只搜索在对称关系中等 价的一种情形,以避免重复搜索对称或相同的系统状态。这种方法称为对称模型 检测[25][27]。 一般来讲能够减少搜索空间的方法能同时节省时间和内存空间的需求。由于 内存空间在某些情况下比时间更为重要,有些方法的目标是以时间换空间。例如 在SPIN[22]中实现的压缩方法和用自动机表示可达状态的方法[28]。 除了在模型检测的过程应用不同方法以增加效率和减少内存空间的需求外, 还有许多研究的目标是减少模型本身或验证性质的复杂性。这方面的方法有:不 同类型的抽象[29][30][31],程序切片[32][33][34],模型分解[35][36],及验 证性质的分解[37]等。抽象的基本想法是抽掉系统中的细节、用尽可能少的状态 来刻划系统的运作过程。程序切片的基本想法是将程序中不影响所要验证的性质 的语句去掉以减少模型复杂性。模型分解的想法是将一个模型分解成若干部分, 或者分别验证,或者提供一个较好的组合方法以降低验证的复杂性。同样,一个 需要验证的性质也有可能分解成若干部分,然后分别验证 克服状态爆炸的另一条途径是限界模型检测( bounded model checking) 57][58]。软件系统状态规模通常极其巨大,应用传统的模型检测方法或符号模 型检测方法都难以见效,而限界模型检测在这方面则有相当的优势[59][60]。限 界模型检测方法的主要思想是检査一个系统在给定的界内是否满足时序逻辑性 质。即,如果要检査M=φ,我们构造一系列M的近似模型M并验证Mk|=φ是 否成立。所构造的近似模型应具有这样的性质:Mk|=中蕴涵M=φ。如果能够在 较小的k时得到验证,则该方法是十分有效的。对于有些用其他方法均由于状态 爆炸而无法处理的问题,限界模型检测方法能够有效验证。目前这方面的硏究十 分活跃[61][62][63][64][65][66]
6 状态空间进行搜索在实际上是不可行的。这就是所谓的状态爆炸问题。 为了能够有效地应用模型检测方法，需要研究减少和压缩状态空间的方法。 文献上关于这方面的文章很多，其中的很多方法已经实现在不同的模型检测工具 中。以下介绍几种常用方法。 符号模型检测的基本原理是将系统的状态转换关系用逻辑公式表示[18]。在 这方法中，二叉图（Binary Decision Diagram〕是用以表示逻辑公式的重要手 段[21]，它能较为紧凑地表示状态转换关系，以降低系统模型所需的内存空间。 另外，状态转换的计算可以以集合为单位，以提高搜索的效率。符号模型检测为 克服“状态爆炸”问题迈出了关键的一步。 On-the-fly 模型检测的基本原理是根据需要展开系统路径所包含的状态， 避免预先生成系统的所有状态[22]。一个系统可以由多个进程组成，并发执行使 得不同进程的动作可以有许多不同的次序。基于对这一问题的认识，我们可以将 某些状态的次序固定，以减少重复验证本质上相同的路径。这种方法称为偏序归 约[23][24]。 由多进程组成的系统中某些进程可能完全类似，并发执行的结果可能产生许 多相同或相似的路径。基于对这一问题的认识，我们可以只搜索在对称关系中等 价的一种情形，以避免重复搜索对称或相同的系统状态。这种方法称为对称模型 检测[25][27]。 一般来讲能够减少搜索空间的方法能同时节省时间和内存空间的需求。由于 内存空间在某些情况下比时间更为重要，有些方法的目标是以时间换空间。例如 在 SPIN[22]中实现的压缩方法和用自动机表示可达状态的方法[28]。 除了在模型检测的过程应用不同方法以增加效率和减少内存空间的需求外， 还有许多研究的目标是减少模型本身或验证性质的复杂性。这方面的方法有:不 同类型的抽象[29][30][31]，程序切片[32][33][34]，模型分解[35][36]，及验 证性质的分解[37]等。抽象的基本想法是抽掉系统中的细节、用尽可能少的状态 来刻划系统的运作过程。程序切片的基本想法是将程序中不影响所要验证的性质 的语句去掉以减少模型复杂性。模型分解的想法是将一个模型分解成若干部分， 或者分别验证，或者提供一个较好的组合方法以降低验证的复杂性。同样，一个 需要验证的性质也有可能分解成若干部分，然后分别验证。 克服状态爆炸的另一条途径是限界模型检测（bounded model checking） [57][58]。软件系统状态规模通常极其巨大，应用传统的模型检测方法或符号模 型检测方法都难以见效，而限界模型检测在这方面则有相当的优势[59][60]。限 界模型检测方法的主要思想是检查一个系统在给定的界内是否满足时序逻辑性 质。即，如果要检查 M|=φ，我们构造一系列 M 的近似模型 Mk 并验证 Mk|=φ是 否成立。所构造的近似模型应具有这样的性质：Mk|=φ蕴涵 M|=φ。如果能够在 较小的 k 时得到验证，则该方法是十分有效的。对于有些用其他方法均由于状态 爆炸而无法处理的问题，限界模型检测方法能够有效验证。目前这方面的研究十 分活跃[61][62][63][64][65][66]
支撑工具的研制 模型检测的优点在于可以完全自动地进行验证,这一方法的成功在很大程度 上应归功于有效的软件工具的支持。以下介绍几个验证不同类型逻辑公式的软件 工具。 SMV[56]是美国卡耐基梅隆大学开发的模型检测工具。用以检测一个有限状 态系统是否满足CTL公式。其系统描述语言为CSM,是一种基于状态转换关系 的描述并发状态转换的语言。SM的典型应用领域包括电子电路的验证。它的建 模方式是以模块为单位,模块可以同步或异步( interleaving)组合。模块描述的 基本要素包括非确定性选择,状态转换和并行赋值语句。其模型检测的基本方法 是以二叉图表示状态转换关系,以计算不动点的方法检测状态的可达性和其所满 足的性质。其后,意大利FBK-IRST和卡耐基梅隆大学合作开发了 NuSMV[26], 在原有的符号模型检测的基本原理上进行了多方面的优化和扩展,这些扩展包括 限界模型检测等功能。 SPIN[22][38]是美国贝尔实验室开发的模型检测工具。用以检测一个有限状 态系统是否满足PL仉L公式及其它一些性质,包括可达性和循环。其系统描述语 言为 Promela,其语法基于进程描述,有类似C语言的结构。SPIN的典型应用领 域包括协议验证。它的建模方式是以进程为单位,进程异步组合。进程描述的基 本要素包括赋值语句,条件语句,通讯语句,非确定性选择和循环语句。其模型 检测的基本方法是以自动机表示各进程和PLTL公式,以计算这些自动机的组合 可接受的语言是否为空的方法检测进程模型是否满足给定的性质。 CWB[39]的不同版本是英国爱丁堡大学和美国北卡洛莱纳州立大学相继开发 的模型检测工具。用以检测系统间的等价关系,PRE- ORDER关系,以及系统是否 满足皿u-演算公式。其系统描述语言为进程代数类型的语言,包括CCS和L0TOS。 这些工具对电子电路、协议、工作流程和程序的验证起到了很好的作用 [3][4][14][1T][108]。由于建模语言的局限性和模型检测方法复杂度较高,这 个工具的可应用性比前面提到的工具要差一些 有些模型检测工具直接面向编程语言,比如贝尔实验室开发的 Verisoft[40 等。模型检测工具很多,其余如牛津大学的FDR[71],斯坦福大学的 Murphi[72] 等,不一一列举。另外,需要一提的是模型检测工具与大型软件开发工具的结合 比如,IBM公司的软件开发工具( Rational tau)、加州大学的 BLAST[73],微软 的SLAM[74]和 Terminator[75],卡内基梅隆大学的 SATABS[76],以及NASA的 Java PathFinder[77]等。这些工具在计算机硬件和协议的验证和检错上取得了 很大的成功[78][79],在验证一些简单的软件性质上也取得了较好的效果 32.带参并发系统的模型检测 非有穷状态系统的典型代表是所谓带参并发系统。带参并发系统实际包含 族并发系统实例,其中以一个(或多个)参数N表示每个系统实例的规模。给定 N的一个具体值,就得到一个具体的并发系统,称为该带参系统的一个实例。带 参系统的难点在于:系统的行为应对参数的任意取值都是正确性的。由于参数的
7 支撑工具的研制 模型检测的优点在于可以完全自动地进行验证，这一方法的成功在很大程度 上应归功于有效的软件工具的支持。以下介绍几个验证不同类型逻辑公式的软件 工具。 SMV[56]是美国卡耐基梅隆大学开发的模型检测工具。用以检测一个有限状 态系统是否满足 CTL 公式。其系统描述语言为 CSML，是一种基于状态转换关系 的描述并发状态转换的语言。SMV 的典型应用领域包括电子电路的验证。它的建 模方式是以模块为单位，模块可以同步或异步(interleaving)组合。模块描述的 基本要素包括非确定性选择，状态转换和并行赋值语句。其模型检测的基本方法 是以二叉图表示状态转换关系，以计算不动点的方法检测状态的可达性和其所满 足的性质。其后，意大利 FBK-IRST 和卡耐基梅隆大学合作开发了 NuSMV[26]， 在原有的符号模型检测的基本原理上进行了多方面的优化和扩展，这些扩展包括 限界模型检测等功能。 SPIN[22][38]是美国贝尔实验室开发的模型检测工具。用以检测一个有限状 态系统是否满足 PLTL 公式及其它一些性质，包括可达性和循环。其系统描述语 言为 Promela，其语法基于进程描述，有类似 C 语言的结构。SPIN 的典型应用领 域包括协议验证。它的建模方式是以进程为单位，进程异步组合。进程描述的基 本要素包括赋值语句，条件语句，通讯语句，非确定性选择和循环语句。其模型 检测的基本方法是以自动机表示各进程和 PLTL 公式，以计算这些自动机的组合 可接受的语言是否为空的方法检测进程模型是否满足给定的性质。 CWB[39]的不同版本是英国爱丁堡大学和美国北卡洛莱纳州立大学相继开发 的模型检测工具。用以检测系统间的等价关系，PRE-ORDER 关系，以及系统是否 满足 mu-演算公式。其系统描述语言为进程代数类型的语言，包括 CCS 和 LOTOS。 这些工具对电子电路、协议、工作流程和程序的验证起到了很好的作用 [3][4][14][17][108]。由于建模语言的局限性和模型检测方法复杂度较高，这 个工具的可应用性比前面提到的工具要差一些。 有些模型检测工具直接面向编程语言，比如贝尔实验室开发的 VeriSoft[40] 等。模型检测工具很多，其余如牛津大学的 FDR[71] ，斯坦福大学的 Murphi[72] 等，不一一列举。另外，需要一提的是模型检测工具与大型软件开发工具的结合。 比如， IBM 公司的软件开发工具(Rational Tau)、加州大学的 BLAST[73]，微软 的 SLAM[74]和 Terminator[75]，卡内基梅隆大学的 SATABS[76]，以及 NASA 的 Java PathFinder[77]等。这些工具在计算机硬件和协议的验证和检错上取得了 很大的成功[78][79]，在验证一些简单的软件性质上也取得了较好的效果 [77][80]。 3.2. 带参并发系统的模型检测 非有穷状态系统的典型代表是所谓带参并发系统。带参并发系统实际包含一 族并发系统实例，其中以一个（或多个）参数 N 表示每个系统实例的规模。给定 N 的一个具体值，就得到一个具体的并发系统，称为该带参系统的一个实例。带 参系统的难点在于：系统的行为应对参数的任意取值都是正确性的。由于参数的