中国科学院软件研究所：模型检测研究进展（朱雪阳、张文辉、李广元、吕毅、林惠民）

模型检测研究进展 朱雪阳张文辉李广元吕毅林惠民 中国科学院软件研究所 计算机科学国家重点实验室 北京100190 目录 摘要 Abstract 1.引言..0 2.典型应用 3.主要研究内容及关键技术 3.1.有限状态模型检测 模态/时序逻辑…11111111114 模型检测算法及其时空效率的改进…… 支撑工具的研制… 32.带参并发系统的模型检测… 33.实时系统的模型检测.18 4.研究进展… 4.1.mu-演算的模型检测 4.2.限界模型检测… 4.3.组合式模型检测 4.4.时间自动机的模型检测 4.5.带参并发系统的模型检测… 4.6.模型检测应用 5.结束语 参考文献…1111114

1 模型检测研究进展 朱雪阳 张文辉 李广元 吕毅 林惠民 中国科学院软件研究所 计算机科学国家重点实验室 北京 100190 目录 摘要 ........................................................................................................................................................................ 2 Abstract ................................................................................................................................................................. 2 1. 引言 ............................................................................................................................................................... 2 2. 典型应用 ..................................................................................................................................................... 3 3. 主要研究内容及关键技术 ................................................................................................................... 4 3.1. 有限状态模型检测 ......................................................................................................................... 4 模态/时序逻辑 ......................................................................................................................................... 4 模型检测算法及其时空效率的改进 ................................................................................................ 5 支撑工具的研制 ....................................................................................................................................... 7 3.2. 带参并发系统的模型检测 ........................................................................................................... 7 3.3. 实时系统的模型检测 .................................................................................................................... 8 4. 研究进展 ..................................................................................................................................................... 8 4.1. mu-演算的模型检测 .................................................................................................................. 9 4.2. 限界模型检测 .............................................................................................................................. 9 4.3. 组合式模型检测 ...................................................................................................................... 10 4.4. 时间自动机的模型检测 ........................................................................................................ 11 4.5. 带参并发系统的模型检测 ................................................................................................... 12 4.6. 模型检测应用 ........................................................................................................................... 12 5. 结束语 ....................................................................................................................................................... 13 参考文献 ............................................................................................................................................................ 14

摘要 保证计算机软硬件系统的正确和可靠是计算机科学与应用中的重要问题。在 为此提出的诸多理论和方法中,模型检测( model checking)以其简洁明了和自动 化程度高而引人注目。模型检测的研究大致涵盖以下内容:模态/时序逻辑、模 型检测算法及其时空效率的改进以及支撑工具的研制。这几个方面之间有着密切 的内在联系。不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往 往是针对某些特定类型的逻辑公式。本文将对模型检测的典型应用、主要研究内 容及关键技术分别加以阐述,最后介绍国内研究人员在该领域的部分新进展。 Abstract How to assure the correctness and reliability of computer hardware and software systems is an important problem of computer science and application. Among theories proposed as solutions to this problem, model checking has become a very attractive and appealing approach, because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics, model checking algorithms, efficiency of mod checking with respect to time and space, and develpment of model checking tools. These aspects are closely related Complexities of model checking algorithms vary very much for different modal/temporal logics; optimizations are often targeted at certain types of logic formulas. We discuss these aspects of model checking as well as some new achievements in this area in China. 1.引言 随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫 的问题。对于并发系统,由于其内在的非确定性,这个问题难度更大。在过去三 十多年间,各国研究人员为解决这个问题付出了巨大的努力,取得了重要的进展。 在为此提出的诸多理论和方法中,模型检测( model checking)[81]以其简洁明 了和自动化程度高而引人注目。 1981年, Clarke和 Emerson提出了描述并发系统性质的时序逻辑CTL,以 及检査有穷状态并发系统是否满足CTL公式的算法,开创了模型检测这一研究方 向[1]。现在模型检测已被应用于计算机硬件、软件、通信协议、控制系统、安 全认证协议等领域,取得了令人瞩目的成功,成为分析、验证并发系统性质的最 重要的技术,并被 Intel、IBM、微软等公司用于生产实践中[2]。模型检测的工 作于1998和2005年两度获得 ACM Paris Kanellakis Theory and Practice

2 摘要 保证计算机软硬件系统的正确和可靠是计算机科学与应用中的重要问题。在 为此提出的诸多理论和方法中，模型检测(model checking)以其简洁明了和自动 化程度高而引人注目。模型检测的研究大致涵盖以下内容：模态/时序逻辑、模 型检测算法及其时空效率的改进以及支撑工具的研制。这几个方面之间有着密切 的内在联系。不同模态/时序逻辑的模型检测算法的复杂性不一样，优化算法往 往是针对某些特定类型的逻辑公式。本文将对模型检测的典型应用、主要研究内 容及关键技术分别加以阐述，最后介绍国内研究人员在该领域的部分新进展。 Abstract How to assure the correctness and reliability of computer hardware and software systems is an important problem of computer science and application. Among theories proposed as solutions to this problem, model checking has become a very attractive and appealing approach, because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics, model checking algorithms, efficiency of model checking with respect to time and space, and development of model checking tools. These aspects are closely related. Complexities of model checking algorithms vary very much for different modal/temporal logics; optimizations are often targeted at certain types of logic formulas. We discuss these aspects of model checking as well as some new achievements in this area in China. 1. 引言 随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性成为日益紧迫 的问题。对于并发系统，由于其内在的非确定性，这个问题难度更大。在过去三 十多年间，各国研究人员为解决这个问题付出了巨大的努力，取得了重要的进展。 在为此提出的诸多理论和方法中，模型检测(model checking) [81]以其简洁明 了和自动化程度高而引人注目。 1981 年，Clarke 和 Emerson 提出了描述并发系统性质的时序逻辑 CTL，以 及检查有穷状态并发系统是否满足 CTL 公式的算法，开创了模型检测这一研究方 向[1]。现在模型检测已被应用于计算机硬件、软件、通信协议、控制系统、安 全认证协议等领域，取得了令人瞩目的成功，成为分析、验证并发系统性质的最 重要的技术，并被 Intel、IBM、微软等公司用于生产实践中[2]。模型检测的工 作于 1998 和 2005 年两度获得 ACM Paris Kanellakis Theory and Practice

Award。2007年,模型检测的创始人 Clarke、 Emerson和 Sifakis共同获得了国 际计算机科学界最高奖-ACM图灵奖。 模型检测的基本思想是用状态迁移系统(S)表示并发系统的行为,用模态/ 时序公式(F)描述系统的性质。这样,“系统是否具有所期望的性质?”就转化 为数学问题“S是否是F的模型?”。对于有穷状态系统,这个问题是算法可判 定的。与其他验证方法相比,模型检测有两个显著的特点:一是可以自动进行, 无须人工干预;二是在系统不满足所要求的性质时,可以生成反例,准确地指出 错误的位置。这两个特点对模型检测在实际应用中的成功起了至为重要的作用 本文将介绍模型检测的典型应用、主要研究内容及关键技术、及国内研究人 员在该领域的部分进展 2.典型应用 早期的模型检测侧重于对硬件设计的验证,随着研究的进展,模型检测的应 用范围逐步扩大,涵盖了通讯协议、安全协议、控制系统和一部分软件。电子线 路设计验证的例子包括:先进先出存储器的验证,验证的性质包括输入和输出的 关系[3];浮点运算部件的验证,验证的性质包括计算过程所需满足的不变式[4]。 对于复杂的协议和软件,模型检测的验证基于抽象和简化的模型,从验证角 度来讲,这并非十分严谨。更为确切的说法应该是协议和软件的分析。协议验证 的例子包括:认证协议的验证,验证的性质包括对通话双方的确认[5][6][7] 合同协议的验证,验证的性质包括公平和滥用的可能性[8];缓存协议的验证 验证的性质包括数据的一致性和读写的活性[9] 由于软件相对比较复杂,并且软件运行中可能到达的状态个数通常没有实质 上的限制,验证通常局限于软件的某些重要组成部分。软件验证的例子包括飞行 系统软件的验证,验证的性质包括系统所处的状态和可执行动作之间的关系 l1][12]:铁路信号系统软件的验证,验证的性质包括控制信号与控制装置状态 的关系[13][14]:数字信号处理算法的缓存分析[10] 测试是保证软件产品可靠性和正确性的传统手段。但它的主要局限性在于: 对给定数据集通过了测试并不能保证在实际运行中对其它输入不发生错误。模型 检测不是针对某组输入,而是面向某类性质来检査系统是否合乎规约。在系统不 满足所要求的性质时,模型检测算法会产生一个反例(一般是一条执行路径)来 说明不满足的原因。这一功能与测试有异曲同工之处。与测试技术相结合,也是 模型检测在软件方面的重要应用[110[111]。 模型检测还可以应用于其它方面,其基本思想是将一个过程或系统抽象成 个有穷状态模型,加以分析验证。这方面的例子包括:化学过程验证,验证的性 质包括阀门、管道和容器的状况[15]:公司操作过程分析,分析的内容包括操作 过程是否具有所需的功能[16];电站操作程序的验证,验证的性质包括操作程序 的动作前后关系和操作是否安全可靠[17]

3 Award。2007 年，模型检测的创始人 Clarke、Emerson 和 Sifakis 共同获得了国 际计算机科学界最高奖--ACM 图灵奖。 模型检测的基本思想是用状态迁移系统（S）表示并发系统的行为，用模态/ 时序公式（F）描述系统的性质。这样，“系统是否具有所期望的性质？”就转化 为数学问题“S 是否是 F 的模型？”。对于有穷状态系统，这个问题是算法可判 定的。与其他验证方法相比，模型检测有两个显著的特点：一是可以自动进行， 无须人工干预；二是在系统不满足所要求的性质时，可以生成反例，准确地指出 错误的位置。这两个特点对模型检测在实际应用中的成功起了至为重要的作用。 本文将介绍模型检测的典型应用、主要研究内容及关键技术、及国内研究人 员在该领域的部分进展。 2. 典型应用 早期的模型检测侧重于对硬件设计的验证，随着研究的进展，模型检测的应 用范围逐步扩大，涵盖了通讯协议、安全协议、控制系统和一部分软件。电子线 路设计验证的例子包括：先进先出存储器的验证，验证的性质包括输入和输出的 关系[3]；浮点运算部件的验证，验证的性质包括计算过程所需满足的不变式[4]。 对于复杂的协议和软件，模型检测的验证基于抽象和简化的模型，从验证角 度来讲，这并非十分严谨。更为确切的说法应该是协议和软件的分析。协议验证 的例子包括：认证协议的验证，验证的性质包括对通话双方的确认[5][6][7]； 合同协议的验证，验证的性质包括公平和滥用的可能性[8]；缓存协议的验证， 验证的性质包括数据的一致性和读写的活性[9]。 由于软件相对比较复杂，并且软件运行中可能到达的状态个数通常没有实质 上的限制，验证通常局限于软件的某些重要组成部分。软件验证的例子包括飞行 系统软件的验证，验证的性质包括系统所处的状态和可执行动作之间的关系 [11][12]；铁路信号系统软件的验证，验证的性质包括控制信号与控制装置状态 的关系[13][14] ；数字信号处理算法的缓存分析[10]。 测试是保证软件产品可靠性和正确性的传统手段。但它的主要局限性在于： 对给定数据集通过了测试并不能保证在实际运行中对其它输入不发生错误。模型 检测不是针对某组输入，而是面向某类性质来检查系统是否合乎规约。在系统不 满足所要求的性质时，模型检测算法会产生一个反例（一般是一条执行路径）来 说明不满足的原因。这一功能与测试有异曲同工之处。与测试技术相结合，也是 模型检测在软件方面的重要应用[110][111]。 模型检测还可以应用于其它方面，其基本思想是将一个过程或系统抽象成一 个有穷状态模型，加以分析验证。这方面的例子包括：化学过程验证，验证的性 质包括阀门、管道和容器的状况[15]；公司操作过程分析，分析的内容包括操作 过程是否具有所需的功能[16]；电站操作程序的验证，验证的性质包括操作程序 的动作前后关系和操作是否安全可靠[17]

3.主要研究内容及关键技术 31.有限状态模型检测 模态/时序逻辑 模型检测中最常用的逻辑有计算树逻辑(CTL- Computation Tree Logic) ]、命题线性时序逻辑(PLTL- Propositional Linear Temporal Logic)[2 和命题皿u-演算[18][19]。其中表示能力最强的是命题皿u-演算。为了实际应用 的需要,出现了这些逻辑的各种(如实时、概率)扩展。以下分别介绍CTL、PLTL 及命题皿-演算 计算树逻辑 一个系统的运行可以看成是系统状态的变化。系统状态变化的可能性可以表 示成树状结构。比如说一个并发系统从一个初始状态开始运行,由于行为的不确 定性,它可以有多个可能的后续状态,每个这样的状态又可以有多个可能的后续 状态,依此类推可以产生一棵状态树。 计算树逻辑CIL是一种分叉时序逻辑。CTL可以描述状态的前后关系和分枝 情况。描述一个状态的基本元素是原子命题符号。CTL公式由原子命题,逻辑连 接符和模态算子组成。CIL的逻辑连接符包括:not(非),or(或),and(与)。 它的模态算子包括:E( Exists a path),A( All paths),X(Next-time),U (Unti1),F( Future),G( Global)。E表示对于某一个分枝,A表示对于所 有分枝,X表示下一状态,U表示直至某一状态,F表示现在或以后某一状态, G表示现在和以后所有状态。前两个算子描述分枝情况,后四个算子描述状态的 前后关系。CIL中描述分枝情况和描述状态的前后关系的算子成对出现,即一个 描述分枝情况的算子后面必须有一个描述状态的前后关系的算子。 CTL公式的产生规则如下:原子命题是CTL公式;如果p,q是CTL公式, yI not p, p or g, p and g, EX p, E(p g, EF p, EG p, AX p, a(pu q) AFp,AGp是CTL公式。例如公式EFp表示:一定会沿某条路径达到一个满足 p的状态。对CIL公式存在线性时间的模型检测算法,即算法的最坏时间复杂度 与|S|F成正比,这里|S|是状态迁移系统的大小,|F是逻辑公式的长度[1]。 命题线性时序逻辑 系统状态变化的可能性既可以看成是一种树状结构,又可以看成是所有可能 的系统初始状态经历各种可能变化的集合,也就是把一颗树看成是有限或无限条 路径的集合。一条路径所代表的是系统的一次可能的运行情况 命题线性时序逻辑关心的是系统的任意一次运行中的状态以及它们之间的 关系。PLIL公式由原子命题,逻辑连接符和模态算子组成。PLTL的逻辑连接符 包括:not,or,and它的模态算子包括:U(Unti1),o( Eventually),a( Always) ◇表示现在或以后某一状态(类似CIL的F),口表示现在和以后所有状态(类 似CTL的G)

4 3. 主要研究内容及关键技术 3.1. 有限状态模型检测 模态/时序逻辑 模型检测中最常用的逻辑有计算树逻辑（CTL－Computation Tree Logic） [1]、命题线性时序逻辑（PLTL－Propositional Linear Temporal Logic）[2] 和命题 mu-演算[18][19]。其中表示能力最强的是命题 mu-演算。为了实际应用 的需要，出现了这些逻辑的各种（如实时、概率）扩展。以下分别介绍 CTL、PLTL 及命题 mu-演算。 计算树逻辑 一个系统的运行可以看成是系统状态的变化。系统状态变化的可能性可以表 示成树状结构。比如说一个并发系统从一个初始状态开始运行，由于行为的不确 定性，它可以有多个可能的后续状态，每个这样的状态又可以有多个可能的后续 状态，依此类推可以产生一棵状态树。 计算树逻辑 CTL 是一种分叉时序逻辑。CTL 可以描述状态的前后关系和分枝 情况。描述一个状态的基本元素是原子命题符号。CTL 公式由原子命题，逻辑连 接符和模态算子组成。CTL 的逻辑连接符包括：not（非）， or（或），and（与）。 它的模态算子包括：E（Exists a path），A（All paths），X（Next-time），U （Until），F（Future〕，G（Global）。 E 表示对于某一个分枝，A 表示对于所 有分枝， X 表示下一状态，U 表示直至某一状态， F 表示现在或以后某一状态， G 表示现在和以后所有状态。前两个算子描述分枝情况，后四个算子描述状态的 前后关系。CTL 中描述分枝情况和描述状态的前后关系的算子成对出现，即一个 描述分枝情况的算子后面必须有一个描述状态的前后关系的算子。 CTL 公式的产生规则如下：原子命题是 CTL 公式；如果 p，q 是 CTL 公式， 则 not p，p or q，p and q, EX p，E(pU q)，EF p，EG p，AX p，A(p U q)， AF p，AG p 是 CTL 公式。例如公式 EF p 表示：一定会沿某条路径达到一个满足 p 的状态。对 CTL 公式存在线性时间的模型检测算法，即算法的最坏时间复杂度 与|S||F|成正比，这里|S|是状态迁移系统的大小，|F|是逻辑公式的长度[1]。 命题线性时序逻辑 系统状态变化的可能性既可以看成是一种树状结构，又可以看成是所有可能 的系统初始状态经历各种可能变化的集合，也就是把一颗树看成是有限或无限条 路径的集合。一条路径所代表的是系统的一次可能的运行情况。 命题线性时序逻辑关心的是系统的任意一次运行中的状态以及它们之间的 关系。PLTL 公式由原子命题，逻辑连接符和模态算子组成。PLTL 的逻辑连接符 包括：not，or，and。它的模态算子包括：U（Until），（Eventually），（Always）。 表示现在或以后某一状态（类似 CTL 的 F）， 表示现在和以后所有状态（类 似 CTL 的 G）

PLTL公式的产生规则如下:原子命题是PLTL公式;如果p,q是PLTL公式, 则notp,porq, p and g,◇p,四p是PTL公式。例如公式Dp表示:某个 时刻后所有的状态都满足p PLTL和CIL的表达能力不同,各有所长。PLTL模型检测的常用方法是将所 要检测的性质即PLTL公式的补转换成 Buchi自动机,然后求其与表示系统的自 动机的交[89][90]。如果交为空,则说明系统满足所要检测的性质;否则生成 个反例,说明不满足的原因[2] 命题m演算 以上介绍的两种逻辑语言关心的是系统的状态以及它们之间的关系。现在我 们介绍一种面向动作的逻辑语言,即皿u-演算。 系统状态的改变总是由某种动作引起的。皿-演算关心的是系统的动作与状 态之间的关系。描述动作的基本元素是动作符号。皿u-演算公式由原子命题,命 题变量,逻辑连接符,模态算子和不动点算子组成。逻辑连接符包括:not,or, and,对于每个动作符号a,有两个模态算子-[a]和。[a]表示对所有的a动 作,表示对某个a动作。不动点算子有最小不动点算子μ和最大不动点算子 m-演算公式的产生规则如下:原子命题和命题变量是m-演算公式:如果p, q是mu-演算公式,则notp,porq, D and q,[a]p,p,μX.p,wX.p是 m-演算公式,例如公式.(por[aX)表示:在任何无穷的a-路径上一定会有 某个满足p的状态 皿-演算的主要缺点是公式不易读懂,其优点是它的表示能力非常强。其表 示能力主要来自于最大与最小不动点的任意交错嵌套。 Bradfield证明了皿u-演 算的交错层次是严格的,即对任意的交错深度d,总存在交错深度为d+1的公式 与任何交错深度不超过d的公式都不等价[54]。CTL和PLTL都可以嵌入到它的 真子集中,并且相应的子集具有与CTL和PLTL相同的复杂度的模型检测算法。 因此很多学者将皿u-演算作为模型检测的一般框架加以研究。 模型检测算法及其时空效率的改进 模型检测算法可分为两类:全局算法与局部算法。全局算法通过遍历系统的 所有状态空间来计算每一个状态所满足的公式;局部算法则从所给定的公式出 发,只搜索为满足该公式所需要查看的那部分状态,因此往往可以提高空间效率。 对于CIL,存在关于系统的状态数和公式长度成线性的检测算法;LTL模型检测 算法的复杂性是多项式空间完备的,目前最好的算法时间复杂度对系统状态数呈 线性而对公式长度呈指数:对于皿u-演算,目前已知的最好的检测算法时间复杂 度关于公式的交错嵌套深度成指数增长;皿u-演算是否存在多项式算法的问题仍 然有待解决[53]。接收无穷对象的自动机是研究模型检测的判定问题和复杂性的 有力工具。近年来,一些学者将模型检测的过程看成双人博弈,取得了有意义的 结果[55]。 模型检测基于对系统状态空间的穷举搜索。对于并发系统,其状态的数目往 往随并发分量的增加呈指数增长。因此当一个系统的并发分量较多时,直接对其

5 PLTL 公式的产生规则如下：原子命题是 PLTL 公式；如果 p，q 是 PLTL 公式， 则 not p，p or q，p and q， p， p 是 PLTL 公式。例如公式 p 表示：某个 时刻后所有的状态都满足 p。 PLTL 和 CTL 的表达能力不同，各有所长。PLTL 模型检测的常用方法是将所 要检测的性质即 PLTL 公式的补转换成 Buchi 自动机，然后求其与表示系统的自 动机的交[89][90]。如果交为空，则说明系统满足所要检测的性质；否则生成一 个反例，说明不满足的原因[2]。 命题 mu-演算 以上介绍的两种逻辑语言关心的是系统的状态以及它们之间的关系。现在我 们介绍一种面向动作的逻辑语言，即 mu-演算。 系统状态的改变总是由某种动作引起的。mu-演算关心的是系统的动作与状 态之间的关系。描述动作的基本元素是动作符号。mu-演算公式由原子命题，命 题变量，逻辑连接符，模态算子和不动点算子组成。逻辑连接符包括：not，or， and，对于每个动作符号 a，有两个模态算子--[a]和。[a]表示对所有的 a 动 作， 表示对某个 a 动作。不动点算子有最小不动点算子 µ 和最大不动点算子 v。 mu-演算公式的产生规则如下：原子命题和命题变量是 mu-演算公式；如果 p， q 是 mu-演算公式，则 not p，p or q，p and q，[a]p，p，µX.p，vX.p 是 mu-演算公式，例如公式 µX.(p or [a]X)表示：在任何无穷的 a-路径上一定会有 某个满足 p 的状态。 mu-演算的主要缺点是公式不易读懂，其优点是它的表示能力非常强。其表 示能力主要来自于最大与最小不动点的任意交错嵌套。Bradfield 证明了 mu-演 算的交错层次是严格的，即对任意的交错深度 d，总存在交错深度为 d+1 的公式 与任何交错深度不超过 d 的公式都不等价[54]。CTL 和 PLTL 都可以嵌入到它的 真子集中，并且相应的子集具有与 CTL 和 PLTL 相同的复杂度的模型检测算法。 因此很多学者将 mu-演算作为模型检测的一般框架加以研究。 模型检测算法及其时空效率的改进 模型检测算法可分为两类：全局算法与局部算法。全局算法通过遍历系统的 所有状态空间来计算每一个状态所满足的公式；局部算法则从所给定的公式出 发，只搜索为满足该公式所需要查看的那部分状态，因此往往可以提高空间效率。 对于 CTL，存在关于系统的状态数和公式长度成线性的检测算法；LTL 模型检测 算法的复杂性是多项式空间完备的，目前最好的算法时间复杂度对系统状态数呈 线性而对公式长度呈指数；对于 mu-演算，目前已知的最好的检测算法时间复杂 度关于公式的交错嵌套深度成指数增长；mu-演算是否存在多项式算法的问题仍 然有待解决[53]。接收无穷对象的自动机是研究模型检测的判定问题和复杂性的 有力工具。近年来，一些学者将模型检测的过程看成双人博弈，取得了有意义的 结果[55]。 模型检测基于对系统状态空间的穷举搜索。对于并发系统，其状态的数目往 往随并发分量的增加呈指数增长。因此当一个系统的并发分量较多时，直接对其

状态空间进行搜索在实际上是不可行的。这就是所谓的状态爆炸问题。 为了能够有效地应用模型检测方法,需要研究减少和压缩状态空间的方法。 文献上关于这方面的文章很多,其中的很多方法已经实现在不同的模型检测工具 中。以下介绍几种常用方法。 符号模型检测的基本原理是将系统的状态转换关系用逻辑公式表示[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 的一个具体值，就得到一个具体的并发系统，称为该带参系统的一个实例。带 参系统的难点在于：系统的行为应对参数的任意取值都是正确性的。由于参数的

取值可以任意多,因此不可能进行穷尽的测试或验证。 带参并发系统的模型检测问题在最一般的情况下是不可判定的[67],但这并 不妨碍人们对某些特定类别且具有重要实际意义的问题取得积极的成果。到目前 为止,国内外学者所提出的带参模型检测方法大体上可分为两类:一是针对某些 特定的带参系统得到判定算法,例如基于对称归约( symmetry reduction)的方 法;二是针对某些重要的时序性质提出可靠但不完备的方法,例如基于抽象 ( abstraction)的模型检测技术。第一种方法中最有代表性的是 Emerson等人 提出的 cutoff方法[68][69][70]。第二种方法中最重要的工作有:基于抽象的 模型检测技术( Abstraction- based Model Checking),组合模型检测技术 ( Compositional Model Checking),以及基于归纳不变量检测( Inductive Invariant Checking)的技术。由于抽象过程往往会损失一些有关系统活性 ( liveness)的信息,因此抽象的方法通常适用于安全性质( safety property) 的验证。 33.实时系统的模型检测 作为模型检测基础的传统模态/时序逻辑可以方便地表示离散事件或状态是 否发生以及发生的先后顺序,而在许多实际应用中人们不仅关心某一事件是否发 生,而且还要求它在确定的时间间隔内发生,例如要求锅炉的水位一旦落到警戒 线时进水阀门必须在3秒钟内开启。这类对相关事件发生的时间有明确要求的系 统称为实时系统。实时系统涉及飞机控制系统、机器人、工业与军事控制系统等 安全性至关紧要的应用领域。 上世纪九十年代以来,实时系统模型检测的研究取得了重大进展,主要表现 在三个方面 1)出现了用于表示实时系统的各种数学模型,如时间 Petri网[411[42],时 间自动机[43][44],以及各种进程代数的时间扩充[45][46]。其中以时间自动机 的影响和应用最为广泛 2)提出能描述实时系统的模态/时序逻辑,如CTL,PLTL和皿u-演算的实时 扩充[47][481[49]。例如实时PTL公式囗=3p表示“在任何时候系统总会在3 个单位时间内达到满足性质p的状态”。 3针对这些实时系统的数学模型和逻辑设计了各种模型检测的算法,并实现 了相应的分析与验证工具,如 Uppal150]、 Kronos[51和 Hy Tech[52]等 4.研究进展 以下重点对国内在皿u-演算性质的模型检测、组合模型检测、限界模型检测、 时间自动机模型检测以及带参并发系统模型检测等方面的理论研究及相关工具 研制的进展,以及模型检测应用方面的研究进展作简单介绍。此外模型检测还有 些重要的研究方向如软件模型检测和概率模型检测等,限于篇幅,这些领域的 进展不再一一阐述

8 取值可以任意多，因此不可能进行穷尽的测试或验证。 带参并发系统的模型检测问题在最一般的情况下是不可判定的[67]，但这并 不妨碍人们对某些特定类别且具有重要实际意义的问题取得积极的成果。到目前 为止，国内外学者所提出的带参模型检测方法大体上可分为两类：一是针对某些 特定的带参系统得到判定算法，例如基于对称归约（symmetry reduction）的方 法；二是针对某些重要的时序性质提出可靠但不完备的方法，例如基于抽象 （abstraction）的模型检测技术。第一种方法中最有代表性的是 Emerson 等人 提出的 cutoff 方法[68][69][70]。第二种方法中最重要的工作有：基于抽象的 模型检测技术（Abstraction-based Model Checking），组合模型检测技术 （Compositional Model Checking），以及基于归纳不变量检测（Inductive Invariant Checking）的技术。由于抽象过程往往会损失一些有关系统活性 （liveness）的信息，因此抽象的方法通常适用于安全性质（safety property） 的验证。 3.3. 实时系统的模型检测 作为模型检测基础的传统模态/时序逻辑可以方便地表示离散事件或状态是 否发生以及发生的先后顺序，而在许多实际应用中人们不仅关心某一事件是否发 生，而且还要求它在确定的时间间隔内发生，例如要求锅炉的水位一旦落到警戒 线时进水阀门必须在 3 秒钟内开启。这类对相关事件发生的时间有明确要求的系 统称为实时系统。实时系统涉及飞机控制系统、机器人、工业与军事控制系统等 安全性至关紧要的应用领域。 上世纪九十年代以来，实时系统模型检测的研究取得了重大进展，主要表现 在三个方面： 1)出现了用于表示实时系统的各种数学模型，如时间 Petri 网[41][42]，时 间自动机[43][44]，以及各种进程代数的时间扩充[45][46]。其中以时间自动机 的影响和应用最为广泛。 2)提出能描述实时系统的模态/时序逻辑，如 CTL，PLTL 和 mu-演算的实时 扩充[47][48][49]。例如实时 PLTL 公式 ≤3 p 表示“在任何时候系统总会在 3 个单位时间内达到满足性质 p 的状态”。 3)针对这些实时系统的数学模型和逻辑设计了各种模型检测的算法，并实现 了相应的分析与验证工具，如 Uppall[50]、Kronos[51]和 HyTech[52]等。 4. 研究进展 以下重点对国内在 mu-演算性质的模型检测、组合模型检测、限界模型检测、 时间自动机模型检测以及带参并发系统模型检测等方面的理论研究及相关工具 研制的进展，以及模型检测应用方面的研究进展作简单介绍。此外模型检测还有 一些重要的研究方向如软件模型检测和概率模型检测等，限于篇幅，这些领域的 进展不再一一阐述

4.1.mu-演算的模型检测 为了对传值并发系统进行模型检测,中科院软件研究所的林惠民等人提出了 阶mu-演算,设计了在符号迁移图上对有穷数据域上的输入变量动态实例化的 模型检测算法,并将其推广到“数据无关( data independent)”的无穷域 [91][92]。基于这个算法实现了一个面向传值并发系统的模型检测工具,并利用 这个工具开展了一系列应用研究。他们还提出了基于谓词的面向移动进程的mu- 演算,并采用对名字空间上的受囿变量动态实例化的策略,首次得到了有穷控制 移动进程模型检测的判定性结果[93ˉ 命题皿-演算的表示能力强于CTL和LTL。这个较强的表示能力主要来源于 最大与最小不动点的任意交错嵌套。与皿u-演算模型检测等价的一个问题是奇偶 博弈的求解。迄今为止所有已经公开发表的mu-演算模型检测和奇偶博弈的求解 算法的复杂度都与公式或博弈图的嵌套深数成指数增长。Mu-演算是否存在多项 式时间的模型检测算法是30年来理论计算机科学中一个尚未解决的难题。中科 院软件研究所的林惠民等提出的奇偶博弈取胜位置集可以分层的理论结果,为解 决mu-演算模型检测是否存在多项式时间算法的问题提供了一条新的途径[94] 国防科学技术大学的刘万伟等提出了一种基于Game理论的mu-演算公式的 可满足性的测试方法,该种方法能够将模态皿u-演算公式的可满足性问题转化为 Focus game的求解问题.进一步,基于这套Game规则,给出了一个新的关于mu- 演算可靠完备的推理系统[95]。 韶关学院的江华等分析了用 Tarski不动点定理计算不动点交替嵌套深度为 4的命题m演算公式的计算过程,找到了计算中间结果间具有的两组偏序关系, 利用这两组偏序关系设计了一个高效的命题mu-演算全局模型检测算法。该算法 与Long等人提出的算法有相似的时间复杂度,但空间复杂度有很大的改进o(dn) 相对于o(n\±{[d/2]+1}),其中n是变迁系统的状态规模,d是命题mu-演算公 式中不动点算子的嵌套深度[96]。 4.2限界模型检测 限界模型检测的研究始于1999年图灵奖获得者 Clarke与合作者提出的基于 存在路径型LTL公式的限界语义及其在模型检测中应用的工作。之后国内外有许 多相关工作。这些工作主要是用同样的思路,发展以限界语义为基础进行较快查 错的方法 中科院软件硏究所的张文辉等人近年来开展用限界模型进行验证的工作,取 得了一系列进展 1)研究了LTL和ACTL的限界验证问题,提出了一种限界验证LTL公式的 不完全的方法[86]。利用类似的基本原理,提出了一种建立在ECTL公 式的限界语义基础上的限界验证ACIL公式的方法[87]。在上述基础上 针对这种不完全的问题,进一步研究了ACIL公式的限界验证问题。提 出了一种建立在ACTL公式的限界语义,并给出了一个ACTL公式完备的

9 4.1.mu-演算的模型检测 为了对传值并发系统进行模型检测，中科院软件研究所的林惠民等人提出了 一阶 mu-演算，设计了在符号迁移图上对有穷数据域上的输入变量动态实例化的 模型检测算法，并将其推广到“数据无关（data independent）”的无穷域 [91][92]。基于这个算法实现了一个面向传值并发系统的模型检测工具,并利用 这个工具开展了一系列应用研究。他们还提出了基于谓词的面向移动进程的 mu- 演算，并采用对名字空间上的受囿变量动态实例化的策略，首次得到了有穷控制 移动进程模型检测的判定性结果[93]。 命题 mu-演算的表示能力强于 CTL 和 LTL。这个较强的表示能力主要来源于 最大与最小不动点的任意交错嵌套。与 mu-演算模型检测等价的一个问题是奇偶 博弈的求解。迄今为止所有已经公开发表的 mu-演算模型检测和奇偶博弈的求解 算法的复杂度都与公式或博弈图的嵌套深数成指数增长。Mu-演算是否存在多项 式时间的模型检测算法是 30 年来理论计算机科学中一个尚未解决的难题。中科 院软件研究所的林惠民等提出的奇偶博弈取胜位置集可以分层的理论结果，为解 决 mu-演算模型检测是否存在多项式时间算法的问题提供了一条新的途径[94]。 国防科学技术大学的刘万伟等提出了一种基于 Game 理论的 mu-演算公式的 可满足性的测试方法，该种方法能够将模态 mu-演算公式的可满足性问题转化为 Focus Game 的求解问题.进一步，基于这套 Game 规则，给出了一个新的关于 mu- 演算可靠完备的推理系统[95]。 韶关学院的江华等分析了用 Tarski 不动点定理计算不动点交替嵌套深度为 4 的命题 mu-演算公式的计算过程，找到了计算中间结果间具有的两组偏序关系， 利用这两组偏序关系设计了一个高效的命题 mu-演算全局模型检测算法。该算法 与 Long 等人提出的算法有相似的时间复杂度，但空间复杂度有很大的改进(O(dn) 相对于 O(n\+{[d/2]+1}))，其中 n 是变迁系统的状态规模，d 是命题 mu‐演算公 式中不动点算子的嵌套深度[96]。 4.2.限界模型检测 限界模型检测的研究始于 1999年图灵奖获得者 Clarke与合作者提出的基于 存在路径型 LTL 公式的限界语义及其在模型检测中应用的工作。之后国内外有许 多相关工作。这些工作主要是用同样的思路，发展以限界语义为基础进行较快查 错的方法。 中科院软件研究所的张文辉等人近年来开展用限界模型进行验证的工作，取 得了一系列进展： 1) 研究了 LTL 和 ACTL 的限界验证问题，提出了一种限界验证 LTL 公式的 不完全的方法[86]。利用类似的基本原理，提出了一种建立在 ECTL 公 式的限界语义基础上的限界验证 ACTL 公式的方法[87]。在上述基础上， 针对这种不完全的问题，进一步研究了 ACTL 公式的限界验证问题。提 出了一种建立在 ACTL 公式的限界语义，并给出了一个 ACTL 公式完备的

有界验证ACIL公式的方法[66],比较了基于命题逻辑公式可满足性判 定的查错和验证与基于BD的模型检测方法的效率和优缺点[88]。 2)在[66]的基础上,完成了CTL公式全集的限界语义定义[98]。该工作的 优点在于能够正确处理限界模型中隐藏的原模型的部分信息,在公式的 限界语义定义中恰当反映公式对限界路径的要求。这样的一种定义有别 于之前的相关工作,使得该限界语义既适合于验证一个性质是否满足又 适合于验证其对偶性质是否满足。同时证明了在一类限制下,不可能定 义可靠和完备的CTL*①LTL和CTL的一种超集)的限界语义,反映了定义 全称路径型限界语义的困难、说明了已有思路在定义合适的CTL*和全称 路径型LTL限界语义方面的不足 3)在上述工作的基础上,研制了基于SAT、验证ACTL性质的限界模型检测 工具 VerBs (httP://lcs.iosac.cn/zwh/verbs/).VerBs的基本策略 是结合CTL限界语义中ACTL和ECTL的语义描述的命题逻辑公式刻画, 用命题逻辑公式可满足性求解的方法或工具对所给定的ACIL性质进行 限界验证或査错。 华南师范大学的杨晋吉等人对验证G(p)和G(p→F(q)编码转换公式进行优 化。通过分析当验证这些模态算子时有限状态机的状态转移和线性时序逻辑的语 义特征,在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有 利于高效编码成SAT实例[99] 清华大学的骆翔宇等提出了在同步的多智体系统中验证时态认知逻辑的有 界模型检测算法。基于同步解释系统语义,在时态逻辑CT*的语言中引入认知模 态词,从而得到一个新的时态认知逻辑 ECKLn.通过引入状态位置函数的方法获 得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及 迁移关系编码。 ECKLn的时态认知表达能力强于另一个逻辑CTLK[100]。 江苏大学的周从华等对线性时态逻辑SE-LTL提出了一种基于SAT的有界模 型检测过程,该过程避免了基于BDD方法中状态空间快速增长的问题;进一步提 出了一种组合了基于SAT的有界模型检测、基于反例的抽象求精、组合推理3 种状态空间约简技术的并发软件验证策略,降低了验证时间和对内存空间的需求 [102]。 国防科学技术大学的虞蕾等提出了PSL(一种用于描述并行系统的属性规约 语言)的限界模型检测方法及其算法框架。他们定义了PSL逻辑的有界语义,而 后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移 关系转换为SAT命题公式,最后验证这两个SAT命题公式合取式的可满足性,这样 就将时序逻辑PSL的模型检测转化为一个命题公式的可满足性问题[101]。 4.3.组合式模型检测 在LTL模型检测技术的研究方面,中科院软件研究所的张文辉等人对一类模 型给出了缓解状态爆炸的方法,即通过分析模型、使用LTL公式刻画不同模式的 运行、将验证问题分解成子问题以降低模型检测空间需求的、基于系统运行路径 集合划分的case- based组合式验证方法[82]。此后,他们又将该方法扩展到更

10 有界验证 ACTL 公式的方法[66]，比较了基于命题逻辑公式可满足性判 定的查错和验证与基于 BDD 的模型检测方法的效率和优缺点[88]。 2) 在[66]的基础上，完成了 CTL 公式全集的限界语义定义[98]。该工作的 优点在于能够正确处理限界模型中隐藏的原模型的部分信息，在公式的 限界语义定义中恰当反映公式对限界路径的要求。这样的一种定义有别 于之前的相关工作，使得该限界语义既适合于验证一个性质是否满足又 适合于验证其对偶性质是否满足。同时证明了在一类限制下，不可能定 义可靠和完备的 CTL*(LTL 和 CTL 的一种超集)的限界语义，反映了定义 全称路径型限界语义的困难、说明了已有思路在定义合适的 CTL*和全称 路径型 LTL 限界语义方面的不足。 3) 在上述工作的基础上，研制了基于 SAT、验证 ACTL 性质的限界模型检测 工具 VERBS（http://lcs.ios.ac.cn/~zwh/verbs/）。VERBS 的基本策略 是结合 CTL 限界语义中 ACTL 和 ECTL 的语义描述的命题逻辑公式刻画， 用命题逻辑公式可满足性求解的方法或工具对所给定的 ACTL 性质进行 限界验证或查错。 华南师范大学的杨晋吉等人对验证 G(p)和 G(p→F(q))编码转换公式进行优 化。通过分析当验证这些模态算子时有限状态机的状态转移和线性时序逻辑的语 义特征，在现有的编码公式的基础上，给出了简洁、高效的递推公式，该公式有 利于高效编码成 SAT 实例[99]。 清华大学的骆翔宇等提出了在同步的多智体系统中验证时态认知逻辑的有 界模型检测算法。基于同步解释系统语义,在时态逻辑 CTL*的语言中引入认知模 态词,从而得到一个新的时态认知逻辑 ECKLn.通过引入状态位置函数的方法获 得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及 迁移关系编码。ECKLn 的时态认知表达能力强于另一个逻辑 CTLK[100]。 江苏大学的周从华等对线性时态逻辑 SE-LTL 提出了一种基于 SAT 的有界模 型检测过程,该过程避免了基于 BDD 方法中状态空间快速增长的问题；进一步提 出了一种组合了基于 SAT 的有界模型检测、基于反例的抽象求精、组合推理 3 种状态空间约简技术的并发软件验证策略，降低了验证时间和对内存空间的需求 [102]。 国防科学技术大学的虞蕾等提出了 PSL（一种用于描述并行系统的属性规约 语言）的限界模型检测方法及其算法框架。他们定义了 PSL 逻辑的有界语义,而 后,将有界语义进一步简化为 SAT,分别将 PSL 性质规约公式和系统 M 的状态迁移 关系转换为 SAT命题公式,最后验证这两个 SAT命题公式合取式的可满足性,这样 就将时序逻辑 PSL 的模型检测转化为一个命题公式的可满足性问题[101]。 4.3.组合式模型检测 在 LTL 模型检测技术的研究方面，中科院软件研究所的张文辉等人对一类模 型给出了缓解状态爆炸的方法，即通过分析模型、使用 LTL 公式刻画不同模式的 运行、将验证问题分解成子问题以降低模型检测空间需求的、基于系统运行路径 集合划分的 case-based 组合式验证方法[82]。此后，他们又将该方法扩展到更