模型检测研究进展 朱雪阳张文辉李广元吕毅林惠民 中国科学院软件研究所 计算机科学国家重点实验室 北京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动 作,<a>表示对某个a动作。不动点算子有最小不动点算子μ和最大不动点算子 m-演算公式的产生规则如下:原子命题和命题变量是m-演算公式:如果p, q是mu-演算公式,则notp,porq, D and q,[a]p,<a>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 动 作， <a>表示对某个 a 动作。不动点算子有最小不动点算子 µ 和最大不动点算子 v。 mu-演算公式的产生规则如下：原子命题和命题变量是 mu-演算公式；如果 p， q 是 mu-演算公式，则 not p，p or q，p and q，[a]p，<a>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]。 模型检测基于对系统状态空间的穷举搜索。对于并发系统，其状态的数目往 往随并发分量的增加呈指数增长。因此当一个系统的并发分量较多时，直接对其