（计算机软件与理论专业论文）基于spin的命题投影时序逻辑模型检查.pdf

摘要 目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重 压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造j 下确可靠的 系统。为了达到上述目标，形式化方法在软件开发中得到了广泛的应用，特别是 模型检查技术。 本文提出了一种基于s p i n 的命题投影时序逻辑的模型检查方法。在此方法中， 系统的性质用命题投影时序逻辑公式来描述，随后这个公式被转换为其永非断言； 然后系统模型用b u c h i 自动机来刻画；最后通过s p i n 完成模型检查，即检查系统 是否满足期望的性质。为了实现这一目的，文中设计并实现了命题投影时序逻辑 公式的解释转换器，以便将命题投影时序逻辑公式自动转换为p r o m e l a 形式的永非 断言。该转换器首先将待验证的命题投影时序逻辑公式转换为其正则式以及正则 图，然后通过正则图可以得到所需的永非断言。将该转换器与模型检查器s p i n 相 结合，使用命题投影时序逻辑公式来在s p i n 中描述系统的性质，这样基于命题投 影时序逻辑的模型检查就能在s p i n 中完成。 关键词：模型检测时序逻辑模型检查器s p i n a b s t r a c t a tp r e s e n t ，t h es o f t w a r ei n d u s t r yi sg o i n gf o r w a r du n d e rd o u b l ep r e s s u r e sf o rm o r e c o m p l i c a t e dp r o d u c tf u n c t i o n sa r er e q u i r e dw h i l es h o r t e rd e v e l o p m e n tp e r i o d sa r eg i v e n am a i nt a r g e to fs o f t w a r ee n g i n e e r i n gi st oe n s u r et h a to n ec a nd e v e l o par e l i a b l e s y s t e mw h i l et h es y s t e mc o m p l e x i t yi si n c r e a s e d f o rt h i sr e a s o n ，f o r m a lm e t h o d sh a v e g o tb r o a da p p l i c a t i o ni ns o f t w a r ed e v e l o p m e n t s ，e s p e c i a l l ym o d e lc h e c k i n gt e c h n i q u e s t h i s p a p e rp r e s e n t s am e t h o df o rm o d e lc h e c k i n gp r o p o s i t i o n a lp r o j e c t i o n t e m p o r a ll o g i cf o r m u l a sb a s e do ns p i n w i t ht h i sm e t h o d ，ap r o p e r t yo fas y s t e mi s s p e c i f i e du s i n gap p t lf o r m u l a t h ep p t lf o r m u l ai s t h e nt r a n s f o r m e dt oan e v e r c l a i m ；f u r t h e r , t h es y s t e mm o d e lw a sr e p r e s e n t e db yal a b e l l e db i i c h ia u t o m a t a ；f i n a l l y , t h em o d e lc h e c k i n gp p t lf o r m u l ai sd o n eb ys p i n t ot h i se n d at r a n s l a t o ri s d e v e l o p e dt ot r a n s f o r map p t lf o r m u l ai n t on e v e r c l a i mu s e dt os p e c i f yt h ep r o p e r t y o fas y s t e m t od os o ，af o r m u l ai s f i r s t l yt r a n s l a t e d i n t oi t sn o r m a lf o r m t h e n ， a c c o r d i n gt ot h en o r m a lf o r m ，an o r m a lf o r mg r a p h o f t h ef o r m u l ai sc o n s t r u c t e d f u r t h e r ， t h en f gi st r a n s f o r m e di n t on e v e rc l a i m w ei n t e g r a t et h ep p t lf o r m u l a st r a n s l a t o r w i t hm o d e lc h e c k e rs p i n ，w h i c hu s e p p t lf o r m u l a st os p e c i f yt h ed e s i r e dp r o p e r t i e s t h e nm o d e lc h e c k i n gp p t lf o r m u l ai sd o n ew i t h i ns p i n k e y w o r d s ：m o d e lc h e c k i n g t e m p o r a ll o g i c m o d e lc h e c k e rs p i n 创新性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不 包含其它人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或 其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做 的任何贡献均已在论文中做了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名：盟日期望竺塞：弓! 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。( 保密的论 文在解密后遵守此规定) 本学位论文属于保密，在一年解密后适用本授权书。 本人签名：二扯 导师签名： 日期望皇墨：皇：! ? 日期坦：至：! 里 兰0 0一_0础竺陵 第一章绪论 1 1 1 存在的问题 第一章绪论弟一早三百v 匕 1 1 研究背景 目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重 压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造正确可靠的 系统。为了达到这个目标，软件测试技术在其中起到了至关重要的作用。 软件测试作为一种实用技术在软件开发中得到广泛的应用，其是保证软件质 量和可靠性的重要手段。但是软件测试只能在耗费大量人力、物力的同时，只能 找出系统中存在的某一部分错误，而并不能找出所有的错误，即不能保证系统是 完全正确的；同时测试过程的效率也依赖于测试人员的经验与系统的规模，且不 能自动的完成；并且随着软件规模的不断增大，功能的不断复杂，特别是在某些 安全关键性系统中，如航空控制系统、卫星发射系统等，其要求软件必须是完全 可靠的，软件测试技术也就显出了其局限性，难以达到用户的需求。因此就需要 一种更加有效的方法来解决这个问题，而能达到这个目标的一种途径就是形式化 片i 士【刈1 3 1 1 3 2 1 3 3 1 j1 、 o 形式化方法和工程界的常规方法相比有着明显的区别。首先，它们的开发原 则不同，形式化方法希望能直接构造出尽可能正确的系统，而常规方法主要是通 过测试来发现系统中的错误。开发原则的不同决定了开发模式的差别，在形式化 方法的开发过程中，需求分析和设计阶段投人了很大的工作量，需要的工作量通 常占软件开发全部工作量的5 5 6 5 ，而编码和测试阶段的工作量相对较小，只 占全部工作量的3 5 一4 5 。而在常规的工程开发方法中，编码和测试阶段所需的 工作量非常大，要占到全部工作量的6 0 7 0 1 2 5 1 。另外，完全的形式化开发方法 是一种理想情况，一般的工程项目只是在部分阶段使用形式化方法，或者是把形 式化方法和其它软件开发方法结合起来使用。 形式化方法是一种用于规范、设计和验证计算机系统的基于数学的方法，包 括各种语言、技术和工具等【2 6 】1 2 7 1 2 s 】【2 9 1 。图1 1 是使用形式化方法规范和验证计算 机系统的示意图， 图1 1 形式化方法示意图 2 基于s p i n 命题投影时序逻辑模型检查 形式化方法可以分为形式规范方法和形式验证方法两大类，形式规范方法包 括各种基于数学的表示法规范语言以及相应的工具；形式验证方法包括各种模型 检查器、定理证明器以及证明和验证的方法等。 规范是一个描述系统及系统特性的过程，形式规范使用规范语言来描述系统， 这种规范语言具有严格数学定义的语法和语义。被描述的系统特性包括行为特性、 时间特性、性能特性及内部结构等。形式规范语言按照描述系统的特性可以分为 三类： 1 描述顺序系统行为的形式规范方法 典型有z 、b 、v d m 3 4 】【3 5 】【3 6 l 。这类方法中的状态使用集合、关系及函数等 数学结构来表示；状态转移使用前置条件和后置条件来表示。 2 描述并发系统行为的形式规范方法 典型有c s p 、c c s ，时序逻辑和i o 自动机1 3 7 1 【3 8 】【3 9 】。这类方法中的状态只使 用简单的数学类型例如整数或对状态根本没有定义；系统的行为用序列、 树或事件的编序关系来表示。 3 集成的形式规范方法 典型有s d l r 和r a i s e i 加】【4 1 1 。它们把两种不同的方法结合起来，既能表示复 杂的状态类型又能描述并发系统的特性。 形式验证是指使用严格的数学方法来推理验证产品或设计是否符合全部或者 部分规范的过程，形式验证要求产品的规范和实现均需要有严格的形式描述。目 前形式验证主要有两种方法：模型检查和定理证明。两种方法都是使用形式化方 法来分析一个系统是否满足所期望的特性。 模型检查是对有限状态系统的一种形式化认证方法，具体做法是：采用一种形 式语言描述系统的规范说明，构造一种算法来遍历根据系统规格说明设计的实现 模型，确认实现模型是否满足系统的规范说明。由于系统的状态是有限的，所以 该算法必然会终止。当前需要解决的问题主要是改进算法和数据结构使其能用于 搜索更大的状态空间。目前有两种比较实用的模型检验方法：第一种是时序逻辑 模型检查，在8 0 年代c l a r k 和q u e i l l e 等人提出了这种方法i 1 引，在这种方法中，规范 说明被表示为一组时序逻辑公式，被验证系统则被表示为有限状态转移的系统模 型，然后构造一个有效的算法来检验一个给定的有限转移系统是否是满足规范说 明的模型；第二种方法是把规范说明表示为一个自动机，被验证系统也被模型化 为一个自动机，然后将被验证系统与规范说明进行比较来确定两者是否一致。v a r d i 和w o l p e r 指出时序逻辑的模型检验问题可以用自动机的术语等价表述，这样就可 以把两种方法统一起来1 1 1 】。 定理证明的原理是：首先我们定义一种数学逻辑，该逻辑系统实际上是一个 形式化的系统，由一系列公理和推理规则组成；然后我们用这种数学逻辑分别表 第一章绪论 3 示被验证系统和其被期望的特性。所谓定理证明就是从系统的公理出发使用推理 规则逐步推导出其所期望特性的证明过程。证明所需要的步骤依赖于系统的公理 和推理规则，在某种程度上也依赖于其派生定义和中间引理。与模型检验不同， 定理证明可直接处理无限的状态空间，它使用类似于结构化的推导过程来证明具 有无限状态的系统。另外值得指出的是，由于大多数定理证明器是交互的，需要 人的参与，因此定理证明的速度相当慢且容易出错，但是从另一方面来说，在完 成证明的过程中，用户的直觉往往起着决定性的作用。 1 1 2 本文的研究方向 作为一种重要的形式化验证技术，模型检查技术是一种自动化的验证技术， 这使得其相对于其他的形式化技术在验证领域的应用中有着很大的优势，也使得 其在软件开发过程中可以得到更为广泛的发展和应用。模型检查技术已经在软硬 件系统、嵌入式系统、通信协议系统的验证等方面取得了成功的应用。 近二十年来，模型检查技术已经得到了长足的发展，并且产生了多种成熟的 模型检查系统，其中比较著名的有基于线性时序逻辑的s p i n 1 6 1 ，基于分支时序逻 辑的s m v 等。而投影时序逻辑i l l 作为命题区间时序逻辑1 9 】的一个扩展，其拥有强 大的表达能力和自然直观的表达形式，在现实应用中更容易使用；并且命题投影 时序逻辑的可判定性问题已经得到证明，这也使得对命题投影时序逻辑公式的模 型检查也变得现实可行【1 9 j 【删。至今，也没有一种基于线性时序逻辑的模型检查器， 这使得研究命题投影时序逻辑的模型检查算法，并开发基于命题投影时序逻辑的 模型检查器变得可行并非常有意义。 1 2 研究现状 本文主要研究基于命题投影时序逻辑的模型检查问题，在其可判定性的基础 上研究其模型检查算法及其相对应的模型检查器的设计与实现。下面分别从模型 检查本身和时序逻辑两个方面来阐述当前的研究现状。 1 2 1 模型检查技术研究现状 模型检查1 2 4 】的概念最早由美国的c l a r k e ，e m e r s o n l l 7 】和法国的j pq u i e l l e ，j s i f a k i s l l 3j 提出的。2 0 世纪8 0 年代初，c l a r k e ，e m e r s o n 等提出了用于描述并发系 统性质的c t l 逻辑，设计了检查有穷状态系统是否满足给定c t l 公式的算法，其 基本思想是用c t l 公式表达程序或电路的时序性质，用f s m 表示程序或电路的状 态转移的抽象结构，通过遍历f s m 来检查时态逻辑公式的j 下确性。模型检查的过 程由下面三部分组成： 4 基于s p i n 命题投影时序逻辑模型检查 ( 1 ) 建模，用模型检查工具可以接收的形式描述系统的可能行为； ( 2 ) 规范，声明系统期望达到的性质，通常用时序逻辑表示； ( 3 ) 验证，由模型检查器自动完成，如果正确则输出确认否则给出相应的反例。 对于指定系统而言，其一般由若干个并行执行的部件组成，系统的状态总数 通常随部件个数的增加而指数级增加，从而引起状态的组合爆炸。为了克服状态 爆炸问题，在1 9 8 7 年，r k u r s h a n 提出了“同念化简”的方法【4 引。其实质就是将复 杂的数据结构和控制序列同态映射到相对简单的数据结构和控制序列，从而减少 了计算复杂度。8 0 年代末，又发展了符号模型检查和二叉判定图( b d d ) 技术1 1 8 l 。 符号模型检查用一个布尔公式表示使它满足的所有状态，而这个布尔公式则以压 缩方式存储在b d d 中，在遍历过程中已经标识的状态也用布尔函数的b d d 表示。 通过适当排列变量的顺序可以大大简化图的结构，这使得模型检查可以处理大规 模的数据结构和控制序列，从而缓和了组合爆炸问题。经过上述的改进，模型检 查方法目前已经达到实用化，并为工业界所接受。 模型检查的优点是完全自动化。如果系统不满足给定的性质，模型检查系统 可以给出反例，从而帮助设计人员找出设计错误。目前已有一些成熟的模型检查 工具，比较著名的有u l 模型检查工具s p i n l l 6 j 和c t l 模型检查工具s m v l l 8 j 等。 模型检查的应用领域不断扩大，除了软硬件设计之外，还包括i e e e 的标准验证、 各种协议验证、大型通信软件验证等。当前对模型检查的研究主要集中在以下三 个方面： 1 对现有的一些模型检查算法进行优化，或者提出一些新的优化算法，更好的 解决模型检查过程中的状态空间爆炸问题，使模型检查器能够对更大规模的问 题或系统进行验证，也使模型检查过程变得更方便而且高效，节省检查的时间 与空间复杂度。现在已经被广泛应用的一些优化算法主要有在s p i n 中采用的基 于偏序关系的优化算法、符号化模型检查方法，在s m v 中采用o b d d 数据结 构的模型检查算法等。这些优化算法都大大增加了模型检查的实用价值，使其 能够被应用到规模的系统当中。 2 将模型检查的思想运用到更广泛的领域中。目前在众多的模型检查算法中， 不仅有一些前面提到的反应系统的模型检查算法，也有针对实时系统的模型检 查算法，比如基于u p p a l 实时系统模型检查算法，基于带时钟的线性时序逻辑 ( l t l c ) 模型检查算法。同时，也有不少学者正在对混合系统的模型检查进行 深入的研究，也取得了一些成果，已经能利用可达性分析对简化的混合系统模 型进行初步的分析与验证。 3 基于新的时序逻辑研究新的模型检查算法，并设计其相应的模型检查器。由 于每一种逻辑都有一定的针对性和独特的应用范围，这也就意味着，使用新的 时序逻辑就扩展了模型检查的应用范围并提高了模型检查的在某些夕i 面的效 第一章绪论 5 率。 1 2 2 时序逻辑研究现状 自从英国学者h o a r e 于1 9 6 9 年提出顺序程序验证以- 来【3 7 】，诸多科学家在程序 验证领域进行了卓有成效的研究，积累了丰富的理论知识和经验，其中包括时序 逻辑、进程代数、p e t r i 网和有穷自动机理论等，并开发了许多实用的工具和环境。 作为其中最重要的一种，时序逻辑也得到了突飞猛进的发展。 当前，时序逻辑主要包括线性时序逻辑1 1 5 l 【矧，分支时序逻辑和区间时序逻辑。 l 1 7 l 是由p n u e l i 于1 9 7 7 年提出来的，经过许多研究人员不断的努力，现已有完 备的公理系统及其证明系统，也有了相应的模型检查算法和基于l t l 的模型检查 器；并且经过不断的扩展已经成功的应用到了实时混合系统的形式验证领域。 c n 最早是由c l a r k e 和e m e r s o n 于1 9 8 0 年引入的，目前基于c r l 的模型检查器 s m v 已经得到了广泛的应用，特别是在针对全局的模型检查领域。现在t i m e dc t l 及其基于c r l 的模型检查器u p p a l 已经被广泛的应用到对实时系统的验证当中。 由英国学者b m o s z k o w s h i 提出的i t l 也在不少学者的不断努力也取了重要的成 果，其公理系统及完备性已经得到了证明1 0 】【2 6 【2 1 】【2 2 】；投影时序逻辑作为r r l 的 扩展，将i t l 从有穷模型扩展到了无穷模型，现在命题投影时序逻辑的可判定性也 得到了证明，为基于p p l 工的模型检查提供了必要的条件【3 】【5 】1 6 j 1 7 11 8 】【1 9 】【2 0 1 。 1 3 本文的研究工作和章节安排 本文主要对基于命题投影时序逻辑模公式的模型检查系统进行研究，并设计 开发了基于s p i n 的p p t l 模型检查器，进而使用该系统完成了对 n e e d h a m s c h r o e d e r 协议验证。 文中首先介绍了模型检查的基本原理及所使用到的模型检查系统s p i n ，然后 介绍了命题投影时序逻辑的基本内容，包括其语法、语义、可满足性问题及其正 则形等，接着重点讨论了基于p p t l 的模型检查的方法及其模型检查器的设计与实 现，并将其与模型检查器s p i n 结合起来，最后通过使用该模型检查系统对一个现 有的通讯协议进行验证。 前面已经对模型检测技术和时序逻辑在程序形式验证中的应用及重要性作了 介绍。本文余下部分的结构如下： 第二章介绍了模型检查技术的基本原理及模型检查系统s p i n ； 第三章介绍了命题投影时序逻辑的语法、语义、投影运算和其它基本公式的 解释，并在此基础上介绍由基本公式所派生的常用公式结构等，并对公式的可满 6 基于s p i n 命题投影时序逻辑模型检查 足性进行简单的讨论； 第四章阐述了基于p p t l 的模型检查方法，重点讨论了如何将一个p p t l 公式 转换为其对应的j 下则式和正则图，进而介绍了投影时序逻辑模型检查器的设计与 实现。 第五章简单介绍了通信协议n e e d h a m s c h r o e d e r ，并使用文中所开发的模型检 查系统对其进行验证，通过该验证实例说明了该模型检查系统如何工作。 最后，是对本文工作的总结和对未来工作的展望。 第二章模型检查 7 第二章模型检查 2 1 模型检查原理 近二十多年来，模型检查作为一种可信且强大的系统自动验证技术得到了广泛 的应用。总体上讲，模型检查就是一些处理步骤，通过这些步骤来判断一个给定 的系统的模型m 是否是指定逻辑公式巾的模型，即m 是否满足巾( mi = 巾? ) 。从直 观上讲，m 为待验证系统的抽象模型，典型的如有穷状态自动机的结构，而巾用时 序逻辑公式或模态逻辑公式来描述，表示系统期望的性质。而模型检查器就是提 供这个步骤的载体，由用户将系统模型和系统期望的性质输入到模型检查器中， 剩下的步骤由模型检查器自动完成。在对系统模型验证完成后，如果不满足则给 出相应的反例，以帮助用户对系统设计中的错误进行定位与修正。如果没有发现 任何错误，用户可以对系统模型的描述进行细化，再重新进行验证，直到达到用 户的要求，图2 1 描述了模型检查的基本方法。由于模型检查器的逻辑表达能力强 大，并且其模型检查过程完全是自动的，这就使模型检查具有强大的吸引力和生 命力。 细化 图2 1 模型检查基本方法 模型检查算法都是基于对系统模型的状态空间进行完全搜索，即检查系统模型 的每一个状态是否行为正确，也就是检查这些状态是否满足期望的性质。其最简 单的形式被称为可达性分析，可达性分析仅仅能证明系统有没有死锁，是否满足 一些系统不变性。可达性分析对于证明系统的一些其他性质并不是很充分，例如 8 基于s p i n 命题投影时序逻辑模型检查 在通信协议当中，系统很关注一条信息发出后，是否最终被接收方收到，而像这 样的系统性质的验证并不能用通常的可达性分析来完成。 在七十年代木八十年代初已经有不少科学家在通信协议的自动化可达性分析 上做了很多工作( w e s t ，1 9 8 2 ) ，并取得了可喜的成果。其中就包括使用有穷状态 自动机的集合来对通信协议进行建模，而自动机之间通过有限的异步消息机制来 进行通信，从初始系统状态出发，通过交换消息，系统所有的可达状态将被确定。 通过这种技术，像x 2 1 、x 2 5 及i b m 的s n a 协议等已经得到了自动化的验训4 引。 模型检查技术实际上可以看作这种早期的用在协议中状态空间搜索技术的一种延 续和发展。与以前的技术相比，模型检查技术能够验证更大范围的性质，并采用 了更加高效的方法来处理状态空间。 2 2 模型检查的主要方法 目前模型检查技术发展十分迅速，其中主要的模型检查方法有两种i l2 j i l 训，它 们的主要区别就在于对系统性质的刻画上： 1 基于逻辑的方法，在这种方法里系统期望的行为通过由逻辑公式描述的系 统性质来保证，通常是时序逻辑公式或者模态逻辑公式。待验证的系统用有穷 状态自动机来描述，一个状态代表变量和控制位置的值，而边则用来表示如何 从一个状态到迁移到下一个状态；如果从系统给定的初始状态出发，能够满足 所期望的性质，则可认为系统是正确的。 2 基于行为的方法，在这种方法里，系统的模型和系统期望的性质用相同的 符号系统来描述，用等价关系或者偏序关系作为系统正确的判定标准。等价关 系表示的意思是两者具有相同的行为，而偏序关系表示至少具有这样的行为。 因为在对如何确定两个进程“具有相同的行为”和“至少具有这样的行为”上 存在着不同的看法，至今已经有几种不同的等价关系和偏序关系的定义。其中 最著名的一种等价的判定方法就是互模拟，即如果一个自动机能够模拟另外一 个自动机的每一步，反之亦然，则称这两个自动机是互模拟的。而最常遇到的 偏序关系就是包含关系，即如果自动机a 所接收的全部的字都能被自动机b 所接收，则自动机b 包含自动机a 。因此如果一个系统的模型与其期望的性质 之间具有等价或者相应的偏序关系，则可称这个系统是正确的。 虽然这两种方法在概念上有所不同，但确有着内在的联系。如果两个模型具有 相同的性质，则它们具有相同的行为，反之亦然。但通常来说，要检查给定逻辑 的所有性质是不太现实的，因此通过互模拟来检查等价性就显得相当有效。 本文所采用模型检查方法是基于逻辑的方法。基于逻辑的方法是起源于q u i e l l e 与s i f a k i s ( 1 9 8 0 ) ，c l a r k e 与e m e r s o n ( 1 9 8 1 ) 两组各自独立的工作。从逻辑上来 第二章模型检查 9 说，这种方法就是要检查系统的描述是否满足时序逻辑公式的模型，所以这种方 法被称为了模型检查。 2 3 模型检查技术的优点及局限性 2 3 1 模型检查技术优点 模型检查技术作为一种快速发展的技术，其得到广泛的使用主要得益于以下的 诸多优点1 1 4 j ： 1 作为一种通用的方法，模型检查技术已经广泛应用到了硬件验证、软件工 程、并发系统、通信协议和嵌入式系统等的验证当中； 2 支持局部验证，系统的设计可以只考虑所有期望性质的一个子集，并用这 个子集对系统进行验证，这使得我们能集中精力在重要的性质上，而不用关心 那些并不重要的方面，这可以大大提高验证的效率； 3 通过模型检查实例研究表明，与模拟和测试相比较，将模型检查引入到系 统的开发过程中并不会延迟系统的开发时间。目前随着模型检查技术的广泛使 用，很多实例已经表明随着模型检查技术的引入系统的开发时间变得更短。另 外，得益于日益先进的优化技术，模型检查器已经能够处理大规模的状态空间； 4 模型检查器能被系统设计者方便的使用，这主要得益于模型检查器不需要 与用户进行太多的交互，只要用户输入系统模型和需求描述，剩下的工作均可 由模型检查器自动完成： 5 在工业界中得到广泛使用，因为模型检查技术在系统开发验证上的实用 性，很多公司均组建了自己的团队来开发相应的模型检查器，如西门子、朗讯 科技等，像i n t e l 和c a d e n c e 也成立了自己的研究团队来进行模型检查技术的 研究，还有一些公司则使用现成的一些模型检查工具，像f u j i t s u ，d u t c hr a i l w a y s 等。这些因素都大大推动了模型检查技术的发展与完善； 6 坚固的数学理论基础，模型与语义理论、并发理论、逻辑与自动机理论、 数据 结构、图论算法等等这些数学理论都为模型检查的发展奠定了坚实的理论基础。 2 3 2 模型检查技术的局限性 虽然模型检查有着众多优点，但是作为一种发展中的技术其也在某些方面存在 着一定的局限性【4 4 i ： 1 模型检查的应用依赖于可判定性问题。在一些特殊的情况下，如无限状态 系统中，模型检查就不能进行有效的计算； 1 0 基于s p i n 命题投影时序逻辑模型检查 2 模型检查只是对实际系统的抽象模型进行验证，而不是对真实的系统进行 验证。这也就会产生这样的现象，系统模型检查得出满足指定的性质，而真实 的系统由于某种原因却并不拥有这样的性质。为此，必须引入一些补充的技术 来克服这些问题，比如语义测试技术； 3 仅仅某些要求检查的性质被验证，但这并不能保证所有期望性质的完备 性，也就是并不是所有的性质得到检验； 4 对系统的抽象和性质进行公式化需要专门的技术，这些工作某种程度上需 要一定的经验； 5 。 像任何软件和工具一样，模型检查器本身可能存在着一些问题，并不是完 全可靠的。但是由于模型检查有着峰实的算法基础，所以可靠性问题并不会造 成严重的问题； 6 不能使用模型检查来验证综合或归纳。例如一个协议用模型检查的方法验 证得知使用1 、2 和3 个进程都是正确的，但是这并不能保证任意n 进程都是 正确的。模型检查只能为后面定理的形式化证明提出建议性参数。 虽然模型检查技术并非十全十美，但是我们相信没有任何人能保证一个现实系 统的绝对正确性。而模型检查却可以大大提高这些系统的可靠性，从这点上来说 模型检查技术的发展与完善是有重要意义的。 2 3 模型检查系统s p i n 模型检查系统s p i n 是由贝尔实验室开发的著名的开源软件，其名称s p i n 为 s i m p l ep r o m e l ai n t e r p r e t e r 的缩写，主要用于分布式协议的形式化验证。该系统最 早开发与1 9 8 0 年，从1 9 9 1 年开始作为开源软件免费提供使用，2 0 0 2 年四月该系 统获得了a c m 的系统软件奖。 模型检查系统s p i n 是基于自动机理论和“o n t h e f l y ”验证技术，用于追 踪如操作系统、数据通信协议、交换系统、并发算法等分布式系统设计中的错误。 该系统可以检查规范中的逻辑一致性、报告死锁、未指定的消息接收、标识不完 整、竞争状态、进程相对速度未保证等问题。 s p i n 系统使用p r o m e l a 作为它的规范说明语言，p r o m e l a 是p r o c e s s m e t a 1 a n g u a g e 的缩写。它不是一种实现软件系统的编程语言，而是一种设计、分 析系统的系统描述语言，这种语言的重点是进程同步与协作的建模，而不是计算 和控制。p r o m e l a 提供了描述分布式系统的必须元素，包括消息发送接收原语、并 发进程并行和异步的组合、通信通道等。 s p i n 有两种工作模式，模拟模式和验证模式。在模拟模式下，可以得到系统 模型的行为快照，但是不能证明我们期望的性质，在验证模式下可以做到这一点。 第二章模型检查 当验证模式发现我们所期望的性质在被验证的模型中无法实现时，s p i n 可以自动 生成相应的反例，这个反例的生成过程是由模拟模式实现的。图2 2 给出了验证模 式的工作流程，如图中所示，在验证流程中用p r o m e l a 语言来对描述系统的模型， 然后将系统模型转化为所有状态均可接收的b u c h i 自动机a s y s ；再用p l t l 公式由 来描述系统期望的性质，然后构造出一巾的b u c h i 自动机a 一巾；然后，构造上述两 个自动机的积自动机，该积自动机代表着违反性质巾的所有计算；最后，通过对积 自动机进行判空，来判定系统模型是否满足公式巾。若模型满足所期望的性质，则 给出相应的确认信息：若模型不满足性质，则通过调用模拟模式给出相应的反例。 图2 2 模型检查器s p i n 验证模式流程 第三章命题投影时序逻辑 1 3 第三章命题投影时序逻辑 本文提出的模型检查方法是基于命题投影时序逻辑进行的，所以本章的内容主 要是对命题投影时序逻辑的语法、语义、解释等进行简单介绍。 投影时序逻辑是一种用于描述离散区间或时段的逻辑系统，它是时序逻辑的一 个分支，是区间时序逻辑的扩展。由于我们只用到其命题部分，所以下面我们只对 命题投影时序逻辑作简单介绍。 3 1 语法 首先假设z 表示整数集，n 表示j 下整数集，n o 表示非负整数集，p r o p 表示原子 公式的集合。 一字母表： 1 ) 可数的原子命题集合p r o p ； 2 ) 符号，、八、o 、鲥 二公式的递归定义： 1 ) 每一个原子命题p p r o p 都是一个公式； 2 ) 如果p ，p 1 ，p m 是公式，那么下面的构造公式也是公式： 1 p 、p la p 2 、o p 、( p l ，o0 9p m ) p r jp 其中o 读作n e x t ，p d 读作p r o j e c t i o n 。 对于指定的公式，如果其中不包含时序操作符( 0 ，p r j ) ，则称这个公式为状 态公式，反之，则称之为时序公式。 3 2 语义 一、状态 构成p t l 区间的是有限或无限的状态序列，我们定义状态s 为从p r o p 到其值 域b = t r u e ，f a l s e l 卜个映射： s ：p r o p _ b 我们使用s i p 来表示原子公式p 在状态s 的值。 二区间 一个区间s = 是一个非空的状态序列，其可以是有穷或无穷区间。它 的长度用i s i 表示，如果区间的长度是无穷的贝j j i s l 等于0 3 ；否则，i s l 等于区问内状态 数减1 ，只有一个状态的区间长度为0 。为了对有穷和无穷的区间有统一的标识符 号，我, f f j 弓i 入一个扩展的整数作为索引，我们定义：n = n o u c o ，并且将比较操 1 4 基于s p i n 命题投影时序逻辑模型检查 作符= ， ，s 扩展到n ，且认定= ，对于任意i n o ，i c o 。为了简化定义，我 们用s 来表示 ，对0 = i ，j = i sj9 我们用s ( i o ) 来表示s 的子区间 ，用s ( k ) 来表示 。一个有穷的区间s 与另外一个区间s 的连接表示了 s s 。 三解释 对于一个p t l 项或公式的解释是一个四元组i = ( s ，i ，k ，j ) ，其中s = 是一个区问，i 、k 是非负整数，j 是整数或c o ，使得i _ k - j = f s i 。我们用( s ，i ，k ，j ) 表 示一个项或公式在子区i 日js ( i i ) 上的解释，这个区间的当前状态为s k 。 公式的可满足关系 - - 递归定义如下： 1 il - p 如果s “p 】为真，如果p 是一个原子命题； 2 ii = ，p 女口果ii p ； 3 i | _ p v q 如果ii - p 且il - q ； 4 ii - o p 如果k j 且( s ，i ，k + l ，j ) i - p ； 5 i l = ( p 1 ，p m ) p r jq 如果存在k = r o = r i - - r m 司使得( s ，i ，r o ，r 0 1 = p l ，( s ，r l - 1 ，r l - 1 ， r i ) l - p l ( 1 1 = m ) ，且对如下两种之一的s ，有( s ，o ，0 ，l s i ) l - q ， ( a ) r m j 且s v = sj ，( r o ，r m ) s ( r m + 1 j ) ； ( b ) r m _ j 且s i - s 、【( r 0 ，r h ) ( o = h = m ) 。 可以知道，il _ p 当且仅当( s ( k j ) ，0 ，o ，j k ) l = p 。如果存在一个解释i 使得ii - p ， 则p 是可满足的。 3 3 可满足性和有效性 p p t l 公式的模型就是一个有穷或者无穷的区间。 区间上的可满足关系定义为t 给定一个区间s ，如果( s ，0 ，0 ，l s1 ) l = p ，则称区间s 满足公式p ，记为s l - p 。如 果存在区间s ，使得s l - p ，那么称公式p 是可满足的：如果对于所有的区间s ，如 果s 1 p ，则称公式是有效的，记为i _ p 。 3 4 导出公式 本节将简要的介绍在后文的模型检查部分将要用到的一些导出公式。在投影时 序逻辑中v ，- ，h ，t r u e ，f a l s e 的定义和经典逻辑相同。 例如： d e f p 1vp 2 = ( p 1ap 2 ) 蔓三童鱼壁墼整堕壁望丝 l 三 - - _ - _ ，。- _ - _ - _ _ _ _ - _ 。_ 。一 埘 p 1 - p 24 p l v p 2 d e f t r u e = pv ，p 耐 f a l s e 一- ，t r u e 下面是一些投影时序逻辑中常用的导出公式： 1 ) e m p t y e m p t y 表示当前状态是区间上的最后一个状态。它的形式语义表示为： ( 口，i ，j , k ) i 暑e m p t y i f f k ；j 根据这个语义，它可以表示成下面形式： a c l e m p t y = 一，o t r u e 2 ) m o r e m o r e 表示当前状态不是区间的最后的一个状态。它的语义可以表示如下： ( 叽f ，k ，川= m o r e i f fk 0 n 满足p l = = p m = p 使，l = p r j ( p 妒。) 。 d；ep e m p t yvp + = v 6 ) 投影操作符p i j ( p l ，p m ) p 巧( p l ，p m ) 表示( p 1 ，p m ) 在一个状态下的投影。 埘 p r j ( p 1 ，p 。) = ( p 1 ，p m ) p r je m p t y 7 ) 并行操作符( 1 1 ) d e f p0q = ( pap r j ( q ，t r u e ) ) v ( qap r j ( p ，t r u e ) ) 这里介绍的并行运算和合取很相似，p l l q 和p a q 的最根本的区别是， 前者允许进程p 和q 指定自己的区间，而后者只能由其中一个进程要么p ， 要么q 来指定区间。例如：l e n ( 2 ) l l l e n ( 3 ) 是可满足的，但是l e n ( 2 ) a l e n ( 3 ) 是不可满足的。 3 5 优先级规则 为了避免过多的使用括号，我们使用下列的优先级规则： 1 1 1 2 )o ，口 3 )八，v ，0 第三章命题投影时序逻辑 1 7 4 ) _ ，h 5 ) ；，p r j 其中优先级从1 到5 依次递减。 3 6 等价关系 我们用p 。q 表示| _ p q ，用p = q 表示i _ 口( p q ) ，前者称为弱等价，后者称为 强等价。类似地，我们用p q 表示| 一p _ q ，称为弱蕴涵。用p d q 表示1 = o ( p - - - , q ) ， 称为强蕴涵。p q 的含义是p 和q 在每个模型的第一个状态下有相同的真假值；而 p = q 的含义是p 和q 在每个模型的所有状态下有相同的真假值。弱蕴涵和强蕴涵有 相似的解释，且强等价或强蕴涵可以推出弱等价或弱蕴涵，但反之不成立。例如， f i r s t t r u e 是成立的，但f i r s t = t r u e 不成立。 第四章命题投影时序逻辑模型检查 1 9 第四章命题投影时序逻辑模型检查 本章将对基于无穷模型的p p t l 公式的模型检查的算法进行详细讨论。为了方 便后面的讨论，我们需要先对p p t l 公式的模型检查的总体方案作简单介绍。 4 1 模型检查p p t l 公式方案设计 在s p i n 的验证模式当中，用p r o m e l a 语言来描述系统的模型，然后将系统模 型转化为所有状态均为可接收的b u c h i 自动机氏，。；再用p l t l 公式巾来描述系统 期望的性质，然后构造出，巾的b u c h i 自动机a ，由；然后，构造上述两个自动机的积 自动机，该积自动机代表着违反性质巾的所有计算；最后，通过对积自动机进行判 空，来判定系统模型是否满足公式由。 基于命题投影时序逻辑的模型检查方法与此十分类似，只是在对系统性质描述 时使用的是命题投影时序逻辑公式，此外两者都是通过系统模型和系统性质转化 为b u c h i 自动机，然后通过自动机的理论来完成模型检查的。如果在我们的这个模 型检查器中也采用p r o m e l a 来对系统模型建模的话，两者除了描述系统性质的逻辑 公式不同外，其他完全相同。因此，我们完全可以将s p i n 扩展，使其支持基于 p p t l 公式的模型检查，也就是说我们在s p i n 当中不仅可以用p l t l 来描述系统 的性质，同样也可以用p p t l 公式来描述系统的性质。因此基于p p t l 公式的模型 检查完全可以在s p i n 中来完成，即使用p p t l 公式代替p l t l 公式来描述系统的 性质。 图4 1 扩展p p t l 公式支持的s p i n 结构模块图 为了实现这一目标，我们需要在s p i n 中加入p p t l 公式的解析模块，及其在 基于s p i n 命题投影时序逻辑模型检查 s p i n 当中实现从p p t l 公式到永非断言的转换模块，其他部分就可以用s p i n 原来 的模块来实现。图4 1 为扩展了对p p t l 公式支持的s p i n 结构模块图，由图4 1 中，我们可知，这个系统总共有9 个模块组成，其中主要包括三个部分，其分别 是系统模型解析与转换部分，系统性质解析与转换部分，及验证部分。只有右上 角的p p t l 公式解析器和转换器模块是新添加，而其他部分的都是使用原有的s p i n 系统。因此，现在我们只需要将p p t l 公式的解析器和转换器设计并实现，然后将 其嵌入到s p i n 当中，就可得到基于p p t l 公式的模型检查器。对