（计算机应用技术专业论文）基于偏序简化的并发系统模型检测技术的研究.pdf

西北大学硕士学位论文 摘要 随着并发软件系统在国民经济、国防等关键领域的广泛应用，如何验证其 正确性和可靠性以保证软件质量成为日益紧迫的问题。对并发系统而言，其内 在的不确定性使问题的难度更大。通过对并发系统的形式化分析，可以查找出 系统设计中的漏洞或缺陷，能够帮助设计者修改和优化系统，使其更规范、有 效、合理。可以说形式化方法在软件系统设计的全过程中发挥相当重要的作用。 模型检测技术是近二十年来最成功的形式化自动验证技术之一。其因自动 化程度高，效率高等优点而被广泛应用于并发系统的分析与验证中。然而模型 检测技术的最大障碍是状态爆炸问题并发系统的状态数量随并发分量的增 加呈指数增长。 因此本文对并发系统进行模型检测技术以及状态爆炸问题进行了深入研 究。主要包括以下四个方面的工作： 首先，分析了目前用于形式化描述的语言。以通信系统c c s 为代表的进程 代数方法，因其概念简洁，可用的数学工具丰富，在并发系统的规范、分析、 设计和验证等方面获得了广泛应用。因此，本文决定采用进程代数的形式化描 述方法来研究并发系统模型。 其次，分析了状态爆炸的成因，将偏序简化技术应用于进程代数模型上。 提出了基于进程代数的偏序简化算法，能更大程度上限制并发系统模型的状态 空间，有效得提高了性质验证的效率。 再次，在偏序简化技术基础上提出了相应的安全性以及死锁性验证算法。 并证明了该算法的有效性。 最后，设计了支持上述算法的模型检测原型系统m c t o o l ，分析了并发模型 的五种进程并发合成简化前后的情况，并使用典型实例，对工具进行了实验验 证。实验结果表明在保证并发系统性质验证结果正确的同时，提高了并发系统 模型检测的效率。 关键词：并发系统，形式化方法，模型检测，偏序简化，进程代数 西北大学硕士学位论文 a b s t r a c t a l o n gw i t ht h ew i d e s p r e a da p p l i c a t i o no fc o n c u r r e n ts o f t w a r es y s t e mi nt h e e s s e n t i a ld o m a i n ss u c ha st h en a t i o n a le c o n o m 5t h en a t i o n a ld e f e n s ea n ds oo n ，t h e p r o b l e mo fh o wt oq u a l i f yc o n c u r r e n ts y s t e m sa c c u r a c ya n dt h er e l i a b i l i t yb e c o m e s ap r e s s i n gt a s k s p e a k i n go ft h ec o n c u r r e n ts y s t e m ，i t si n t r i n s i cu n c e r t a i n t ym a k e s t h ep r o b l e mm o r ed i f f i c u l tt h a ne v e r w i t ht h ea n a l y s i so ft h ec o n c u r r e n ts y s t e mb y u s i n gf o r m a lm e t h o d ，i tc a l ls e a r c ht h el o o p h o l eo rt h ef l a w si nt h es y s t e md e s i g n ， a n ds oc a nh e l pt h ed e s i g n e r sr e v i s ea n dt h e no p t i m i z et h es y s t e m ，f i n a l l ym a k e st h e s y s t e mt ob em o r en o r m a t i v e ，m o r ee f f e c t i v ea n dm o r er e a s o n a b l e i no t h e rw o r d s ， t h ef o r m a lm e t h o dp l a y st h eq u i t ev i t a lr o l ei nt h ee n t i r ep r o c e s so fs o f t w a r es y s t e m d e v e l o p m e n t m o d e lc h e c k i n gi so n eo f t h em o s ts u c c e s s f u la u t o m a t i cv e r i f i c a t i o nt e c h n i q u e s i nt h ep a s tt w od e c a d e s b e c a u s eo fi t sh i g hl e v e la u t o m a t i o na n dh i 【g he f f i c i e n c y , m o d e lc h e c k i n gh a sb e e nw i d e l yu s e di nt h ea n a l y s i sa n dv e r i f i c a t i o no fc o n c u r r e n t s y s t e m h o w e v e rp r a c t i c a la p p l i c a t i o no fm o d e lc h e c k i n gt or e a ls y s t e m sh a sb e e n s t y m i e db yt h es t a t ee x p l o s i o np r o b l e m ，a ne x p o n e n t i a lg r o w t hi nt h en u m b e ro f s t a t e st ob ee x p l o r e da st h en u m b e ro fp r o c e s s e sw h i c hc o m p o s e dt h es y s t e m i n e r e a s e s a r e ri n v e s t i g a t i n ga n da n a l y z i n gt h ec a u s eo fs t a t ee x p l o s i o np r o b l e ma n dt h e m o d e lc h e c k i n gt e c h n o l o g yt a i l e df o rc o n c u r r e n ts y s t e m ，m u c hr e s e a r c hh a sb e e n d o n e t h em a i nc o n t r i b u t i o n si nt h i st h e s i sa r ei nt h ef o l l o w i n g ： f i r s t l y , c c s ，s h o r tf o rc a l c u l u so fc o m m u n i c a t i o n 墅v s t e m ，a so n eo ft h em o s t f a m o u sp r o c e s sa l g e b r a su s e di nf o r m a lm e t h o d ，i ss t u d i e d b e c a u s eo fi t ss u c c i n c t c o n c e p ta n dr i c hs u p p o r t i n gt o o l sa v a i l a b l e ，i th a sb e e no b t a i n e dt h ew i d e s p r e a d a p p l i c a t i o ni na l la s p e c t so fb u i l d i n gc o n c u r r e n ts y s t e m ，s u c ha sc r i t e r i o n ，a n a l y s i s ， d e s i g n ，c o n f i r m a t i o na n ds oo n s ot h ec c s a st h ef o r m a ld e s c r i p t i o nm e t h o di su s e d i nt h i sp a p e rt os t u d yt h ec o n c u r r e n ts y s t e mm o d e l t t 西北大学硕士学位论文 s e c o n d l y , t h ec a u s e so fs t a t ee x p l o s i o np r o b l e ma n dp a r t i a l - o r d e rr e d u c t i o n t e c h n o l o g yt a i l e df o rc o n c u r r e n ts y s t e m sa r es t u d i e d p a r t i a l o r d e rr e d u c t i o nm e t h o d b a s e do np r o c e s sa l g e b r ai s p r o p o s e d ，b yw h i c hm o r er e d u n d a n ts t a t e sc a l lb e r e d u c e da n dt h ee f f i c i e n c yo f v e r i f i c a t i o nc a nb ee f f e c t i v e l ye n h a n c e d t h i r d l y , t h ev e r i f i c a t i o na l g o r i t h m so fs a f e t yp r o p e r t ya n dd e a d l o c ku s i n g p a r t i a l o r d e rr e d u c t i o nt e c h n o l o g ya r ep r o p o s e d a n dt h e s ea l g o r i t h m sh a v eb e e n p r o v e nv a l i d i t y a tl a s t ，as u p p o r t e dt o o lm c t o o l ( m o d e lc h e c k i n gt 0 0 1 ) i si m p l e m e n t e dt o v e r i f yc o n c u r r e n ts y s t e m t h ef i v ek i n d so fc o m b i n a t i o nm o d e lf o rc o n c u r r e n t p r o c e s s e sh a v e b e e na n a l y z e d a n dt h et y p i c a lc o n c u r r e n c ym o d e l sh a v eb e e nt e s to n m c t o o lf o re x p e r i m e n t ，a n dt h er e s u l t ss h o wt h a tw h i l eg u a r a n t e e i n gt h ec o l t e c t n e s s o fv e r i f i c a t i o nr e s u l t s ，p a r t i a l - o r d e rr e d u c t i o nt e c h n i q u ee n h a n c e st h ev e r i f i c a t i o n e f f i c i e n c yi nd e e d k e y w o r d s ：c o n c u r r e n ts y s t e m ，f o r m a lm e t h o d ，m o d e lc h e c k i n g ，p a r t i a l - o r d e r r e d u c t i o n ，p r o c e s sa l g e b r a i i i 西北大学学位论文知识产权声明书 本人完全了解学校有关保护知识产权的规定，即：研究生在校攻 读学位期间论文工作的知识产权单位属于西北大学。学校有权保留并 向国家有关部门或机构送交论文的复印件和电子版。本人允许论文被 查阅和借阅。学校可以将本学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学 位论文。同时，本人保证，毕业后结合学位论文研究课题再撰写的文 章一律注明作者单位为西北大学。 西北大学学位论文独创性声明 本人声明：所呈交的学位论文是本人在导师指导下进行的研 究工作及取得的研究成果。据我所知，除了文中特别加以标注和 致谢的地方外，本论文不包含其他人已经发表或撰写过的研究成 果，也不包含为获得西北大学或其它教育机构的学位或证书而使 用过的材料。与我一同工作的同志对本研究所做的任何贡献均已 在论文中作了明确的说明并表示谢意。 学位论文作者签名：工婷 ? i j 、) 7 年占月斗日 西北大学硕士学位论文 第1 章引言 1 1 研究的背景和意义 伴随着网络规模的不断扩大以及并发分布式系统的迅速发展，并发分布式 计算研究成为当今计算机科学与技术中重要的发展方向之一。对并发分布式计 算的研究不仅具有理论意义，同时具有实践意义，理论与实践的同步发展，既 可以用实践推动理论同时又可以用理论来指导实践。 高质量软件是软件理论研究和工程实践领域共同关注的焦点，在方法上主 要着眼于应用需求、设计模型和软件实现三方面之间的联系。如通过建立在严 格数学理论基础上的形式化方法对并发软件行为和性质的准确刻画，来验证系 统设计模型是否满足既定的应用需求【1 】；而测试则通过运行软件实现来考察其 是否符合设计模型或者是否满足既定的应用需求。这样，通过在需求分析、设 计和开发的不同环节上多种方法的相互配合，为实现高质量软件提供有力的保 障。目前，保证软件质量主要是通过测试和模拟等方法。但是，由于测试用例 的覆盖率是有限的，而且系统的运行通常与外部环境有关，因此测试是有困难 的，不仅花费很大，而且无法保证发现潜在的错误。形式化方法对并发分布式 计算理论模型研究主要是将涉及分布与并发行为的各种概念形式化，从而给出 这些行为的精确定义，避免系统开发人员理解上的二义性，并且为系统开发人 员提供可靠的数学工具，用于说明、设计和验证并发系统的多个方面，如系统 运行的正确性、安全性等。可见，为了从根本上保证软件系统的可靠安全，采 用形式化方法对系统进行形式化验证和分析是构造安全可靠软件的一个重要途 径【2 】。 随着计算机软硬件系统日益复杂，特别是对于并发分布式系统，其本身就 非常复杂，开发过程不仅难度大、效率低而且周期长，因此很难避免和发现其 中隐含的错误和缺陷。软件是否可信赖已经成为一个国家的经济、国防等系统 能否正常运转的关键因素之一，尤其在一些诸如航空航天、核反应堆控制等安 全悠关( s a f e t yc r i t i c a ls y s t e m s ) 的领域更是如此，其失误和崩溃可能会造成生命和 西北大学硕士学位论文 财产的重大损失，甚至导致灾难。因此这类系统要求绝对安全可靠，不容半点 疏漏。如何确保这些系统的可靠性成为计算机科学领域中共同关注的一个焦点 问题【3 】。特别是对并发分布式系统而言，其内在的不确定性使问题的难度更大。 随着实际问题的复杂度提高，通过形式化的方法来解决问题的需求变得越 来越强烈。运用形式化方法对并发分布式软件系统进行分析和验证，是计算机 科学基础研究中的一个前沿方向。形式化方法原则上就是采用数学与逻辑的方 法描述和验证系统。形式化的过程始于描述而终于分析。一个形式化方法的最 初目标就是完整的、准确的、无二义的描述；而最终的目标是对已经用形式化 语言描述好的系统进行分析，从而对系统的正确性、安全性等问题做出准确的 判断。 形式化验证主要包括定理证明( t h e o r e mp r o v i n g ) 和模型检测( m o d e lc h e c k i n g ) 等方法。定理证明通过演绎推理证明软件的正确性，但推理过程往往需要人工 参与以使推理向正确的方向进行。其不足之处就是不能做到完全自动化验证， 人为的推理过程十分烦琐，费时费力，因此在实际应用中的影响有限。而模型 检测以其简洁明了和自动化程度高而引人注目。 模型检测使用状态空阿搜索的办法来自动地检验一个有穷状态系统是否满 足其设计规范。其基本原理是，用状态迁移图s 表示所要分析的系统，用模态 时序逻辑公式妒描述所要检查的性质。系统是否具有所要求的性质就归结为 s | = 矿是否成立，对有限状态系统，这个问题是可判定的。与其他验证方法相 比，如模拟、测试、机器证明等，模型检测方法有诸多优点，主要体现为：验 证过程完全自动化；当抽象模型不满足逻辑公式时，检测工具会自动产生一个 反例，说明为什么不满足，以用于查错和修改。诊断信息的生成是模型检测方 法的重要组成部分。好的诊断信息不仅有利于人们对问题的理解，更有助于在 模型不满足逻辑性质时找到问题并排除错误。 并发分布式软件系统设计上的缺陷在软件开发后期往往很难修复，为此在 开发周期及成本方面付出的代价很高。而软件质量与其设计缺陷有着密不可分 的联系。形式化方法的引入正是为了尽早地发现软件设计上的缺陷。运用形式 化方法对并发软件系统进行分析和验证，是计算机科学基础研究中的一个前沿 2 西北大学硕士学位论文 方向，为实现高质量软件提供有力的保障。通过对软件系统的形式化分析，可 以将软件系统非形式化规范转化为具有严格语义的形式化描述，从而便于系统 设计人员阅读、理解、修改、验证和设计开发。可见，从软件系统的形式模拟 与验证到实际的开发应用，形式化方法都起着一个重要的桥梁作用。 1 2 模型检测技术的研究现状和问题 并发分布式系统开发人员缺乏方法学的指导是当前阻碍分布式应用发展的 瓶颈之一。当前面向对象软件开发方法学已成为主流，近年来涌现出许多面向 对象分析与设计方法，例如b o o c h 、c o a d y o u r d o n 、o o s e 、o m t 、w t r f s - b r o c k 等方法，这些方法在基本概念、表示技术、开发过程、支持工具等各有千秋。 对象管理组织( o b j e c tm a n a g e m e n tg r o u p ，o m g ) 采纳并发布了统一建模语言 ( u m l ) 作为面向对象分析与设计表示技术的规范标准。然而这些软件开发方法 并未专门针对并发软件系统的特点而制订，导致系统开发人员在应用这些开发 方法时仍需要不断尝试与探索，造成并发分布式软件系统开发成本与风险的增 大。虽然u m l 也定义了用于描述系统行为的交互图、活动图等等，但都缺乏 精确的行为语义，而在描述系统的行为上存在着片面性：交互图中的顺序图描 述的仅仅是系统活动的一个顺序脚本，不能反映不确定选择和并发行为；而活 动图则强调的是活动到活动的控制流，缺乏对活动参与对象及其状态的描述， 而且这些方法也不能对系统进行形式化的验证。 形式化验证主要包括定理证明( t l l e o r e mp r o v i n g ) 和模型检澳 ( m o d e lc h e c k i n g ) 等方法。定理证明通过演绎推理证明软件的正确性，但推理过程往往需要人工 参与以使推理向正确的方向进行。 模型检测的研究始于八十年代初，当时c l a r k e ，e m e r s o n 等人提出了用于 描述并发系统性质的c t l ( c o m p u t a t i o nt r e el o g i c ) 公式的算法，并实现了一个 原型系统。这一工作为对并发系统的性质自动进行验证开辟了一条新的途径， 成为近二十年来计算机科学基础研究的一个热点。模型检测已被应用于计算机 硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令 人瞩目的成功，并从学术界辐射到了产业界。许多大公司，如i n t e l 、h p 、p h i l l i p s 3 西北大学硕士学位论文 等成立了专门的小组负责将模型检测技术应用于生产过程中。b r y a n t 、c l a r k e 、 e m e r s o n 和m c m i l l a n 因模型检测的创始性工作获得了1 9 9 8 年a c mp a r i s i g m e l l a k i sa w a r df o rt h e o r ya n dp r a c t i c e 模型检测的主要困难是状态空间爆炸问题，即在把并发系统显式的表示为 状态迁移系统时，其状态数量随并发分量的增加呈指数增长。因此，当一个系 统的并发分量较多时，直接对其状态空间进行搜索在实际过程中是不可行的。 这就是所谓的状态爆炸问题。 状态爆炸问题往往出现在进程并发合成环节上，若能限制与子系统交互的 环境就能控制其状态规模。普度大学的w e ij e ny e h 旧提出通过改造并发模型进 程代数的定义来控制进程组合中间过程的状态爆炸技术。 然而子系统交互环境也可以不需要开发者定制，否则可达性分析的自动化 程度就会降低。n a s a 的a m e s 研究中心的d i m i t mg i a n n a k o p o u l o u 和c o r i n a s p a s a r e a n u 川”伽提出自动化程度更高的组合可达性分析技术假设一保证 ( a s s u m e - g u a r a n t e e ) 推理。它借助假设( a s s u m e ) 自动推导出与子系统交互的环 境，不仅能够有效控制组合过程中的状态规模，又能够验证系统是否满足性质。 b e l l 实验室的p a t r i c eg o d e f i o i d 。m 邮”仔细研究了并发模型中进程间迁移的 依赖关系，提出针对状态爆炸的偏序简化技术，在p e t r i 网描述的并发模型上得 到了很好的应用，但至今还未在进程代数描述的模型上得以应用。本文主要将 偏序简化技术与进程代数结合起来进行模型检测技术的研究。 1 3 主要研究内容 有关分布式计算理论研究的主要目的是将涉及分布与并发行为的各种概念 形式化，从而给出这些行为的精确定义，避免系统开发人员理解上的二义性， 并为系统开发人员提供可靠的数学工具，用于说明、设计和验证并发分布式系 统。显然，开发并发分布式系统比传统的集中式系统更需要一种精确的数学模 型。在此基础上，采用形式化方法对系统进行形式化验证和分析是构造安全可 靠软件的一个重要途径。 模型检测的好处在于它有全自动化的检测过程，并且如果一个性质不满足， 4 西北大学硕士学位论文 它能给出这个性质不满足的理由。系统开发人员即可据此对所开发的系统描述 进行改进。模型检测的最主要的困难是所面临的组合爆炸的问题。 结合课题背景，本文的研究内容主要包括以下四个方面： 分析了形式化描述的多种方法。由于r o b i nm i m e r 提出来的并发计算模型 进程代数描述方法，抓住了并发的基本特质，因而能够比较好的描述并发 系统的功能，因此确定了本文所研究的模型检测的形式化描述方法采用基于通 信系统演算的方法c c s ，即进程代数的方法。 针对状态爆炸的问题，主要做以下研究：分析状态爆炸的成因，研究形式 化描述语言进程代数、偏序简化技术，以及基于进程代数模型上的偏序简化技 术。针对传统偏序简化出现的一系列的问题，改进算法，并提出确定迁移优先 选择的简化算法策略。通过有效的简化算法，提高模型检测效率。 研究对并发系统进行性质验证的方法，提出检测并发系统中的安全性以及 死锁性的性质验证算法。 根据基于进程代数的偏序简化技术、安全性以及死锁性的验证方法，设计 出模型检测的支持工具m c l 如i ，实现对并发分布式系统模型的简化以及性 质验证。 1 - 4 本文结构及章节安排 本文内容安排如下： 第一章为引言部分，简要说明了此研究工作的相关背景、国内外该领域研 究现状和问题以及主要研究的内容。 第二章介绍了形式化方法和模型检测的相关理论以及模型检测中面临的主 要问题。 第三章介绍了解决状态空间爆炸问题的偏序简化技术以及一种形式化描述 方法通信系统演算c c s 理论，并研究了基于进程代数模型的偏序简化技术。 第四章介绍并详细说明了模型检测系统的原型验证工具m c t o o l 的设计， 系统结构、输入语言m c t l 、核心算法以及实现，提出了基于偏序简化技术的 状态化简算法以及安全性和无死锁性的性质验证方法。 5 西北大学硕士学位论文 第五章介绍了模型检测系统的原型验证工具m c t o o l 的实例研究，用实例 说明了其基于模型检测语言m c t l 的偏序简化技术的有效性以及验证安全性的 结果。 第六章结束语，总结了论文的研究成果，并对后续的研究工作做出规划。 6 西北大学硕士学位论文 第2 章并发系统的模型检测 2 1 并发系统 并发指的是多个活动同时发生的现象。简单的说，具有多个并发行为的系 统都可称为并发系统。从紧密耦合的并行系统到松散耦合的分布式系统，都可 以看作是并发系统。直观得看，并发系统具有区别于串行系统的许多特征。首 先，在并发系统中往往有多个计算主体同时执行，使得主体之间可能发生意想 不到的相互作用，例如冲突、死锁、竞争等等。其次，许多并发系统同时也是 交互系统，程序在输出结果后往往不终止，通信和交互的过程往往需要不断地 进行；并且在同一时刻，往往有多个实体在进行信息的交换。此外，并发程序 往往是不确定的，也就是说并发程序的执行结果( 顺序) 不仅依赖于输入数据而 且受环境的影响，相同的输入可能得到不同的输出。这些特征使得传统的针对 串行计算的理论和模型不再适用于并发计算。因此，对并发系统的建模和验证 更加困难。活性、安全性、公平性等性质是对并发系统的特别要求。这些性质 可以用模型检测的工具进行验证。 在这样的背景下，各种并发理论相继提出并得到广泛研究，例如，p e t r in e t 、 进程代数、模态逻辑等。其中最有代表性的工作之一是r o b i n m i l n e r 提出的c c s 进程演算理论及其各个变种。它们包括纯c c s ( p u r ec c s ) “”，传值 c c s ( v a l u e - p a s s i n gc c s ) ，丌演算n 4 ”和界程演算等等。在并发系统中，需 要解决的问题很多，例如通讯实体之间传送数据带来的问题，以及进程发生移 动所带来的问题，这些都是当前并发领域研究的热点和难点所在。 2 2 形式化方法概述 2 2 1 并发系统形式化描述的必要性 由于并发系统本身非常复杂，因此其开发过程不仅难度大、效率低、周期 长，而且很难避免和发现其中隐含的错误和缺陷。形式化方法被公认为是一种 行之有效的减少设计错误、提高系统可信度的重要途径。 7 西北大学硕士学位论文 形式化方法是指有完备的数学基础，并且这种数学基础不仅提供了精确定 义的方法，具有一致性、完整性等特征，而且也提供了不需运行系统就可证明 其性质的方法。形式化的过程始于描述而终于分析。一个形式化方法最初的目 标就是完整的、准确的、无二义的描述；而最终的目标则是对已经用形式化语 言描述好的系统进行分析，从而对系统的正确性、安全性等问题做出正确的判 断。 形式化方法支持大型复杂的软件系统的形式模拟和验证，它可以将软件系 统非形式化规范转化为具有严格语义的形式化描述，从而便于系统设计人员阅 读、理解、修改、验证和设计开发。因此，从软件系统的形式模拟与验证到实 际的开发应用，形式化方法都起着一个重要的桥梁作用。通过对并发系统的形 式化分析，可以查找出系统设计中的漏洞或缺陷，能够帮助设计者修改和优化 系统，使其更规范、有效、合理。 形式化方法对分布式计算理论模型研究主要是将涉及分布与并发行为的各 种概念形式化，从而给出这些行为的精确定义，避免系统开发人员理解上的二 义性，并且为系统开发人员提供可靠的数学工具，用于说明、设计和验证并发 系统的多个方面，如系统运行的正确性、安全性等。显然，开发并发分布式系 统比传统的集中式系统更需要一种精确的数学模型。 形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件要求 的描述。软件要求的描述是软件开发的基础。比如说一般非形式化的描述很可 能导致描述的不明确和不一致。如果描述的不明确和不一致导致设计、编程的 错误，将来的修改所要付出的代价就非常大了。如果导致的错误没有被发现， 则影响程序的可靠和使用。形式化方法则要求描述的明确性，而描述的不一致 性也就相对易于发现。其次是对软件设计的描述。软件设计的描述和软件要求 的描述一样重要。形式化方法的优点对于软件要求的描述同样适用于软件设计 的描述。另外由于有了软件要求的形式化描述，就可以检验软件的设计是否满 足软件的要求。对于编程来讲，就可以考虑自动代码生成。对于一些简单的系 统，形式化的描述有可能直接转换成可执行程序，这就简化了软件开发过程， 节约了资源和减少了出错的可能性。另外，形式化方法可以用于程序的验证， 以保证程序的正确性。对于测试来讲，形式化方法可用于测试用例的自动生成， 8 西北大学硕士学位论文 这可以节约许多时间和在一定程度上保证测试用例的覆盖率。 2 2 2 形式化方法研究的主要内容 形式化方法的主要目的是要把软件开发过程建立在严密可行的数学基础之 上，从而提高软件质量和软件生产率。 形式化方法的一个重要研究内容是形式化规范( f o r m a ls p e c i f i c a t i o n ) ，它是 对程序。做什么”( w h a tt od o ) 的数学描述，是用具有精确语义的形式化语言书 写的程序功能描述，它是设计和编制程序的出发点，也是验证程序是否正确的 依据。 形式化方法的另一重要研究内容是形式验证( f o r m a lv e r i f i c a t i o n ) 。形式验证 与形式化规范之间具有紧密的联系，形式验证就是验证已有的系统p ，是否满 足其规范( 0 ，咖的要求( 即p ( o ，咖) ，它也是形式化方法所要解决的核心问题。 形式化方法原则上就是采用数学与逻辑的方法描述和验证系统。其描述主 要包括两方面：一是系统行为的描述，也称建模( m o d e l i n g ) 。通过构造系统的模 型来描述系统及其行为模式；二是系统性质的描述，也称规范或规约 ( s p e c i f i c a t i o n ) ，即表示系统满足的一些性质如安全性、活性等。 由于形式化方法能在早期发现系统中的不一致、歧义、不完全和错误等问 题，目前已被证明是一种行之有效的减少设计错误、提高软件系统可信性的重 要途径。形式化方法的意义在于它能帮助发现其他方法不太容易发现的系统描 述的不一致、不明确或不完整之处，有助于增加软件开发人员对系统的理解。 因此，形式化方法是提高软件系统，特别是安全悠关( s a f e t y - c r i t i c a l ) 系统的安全 性和可靠性的重要手段【埘。 2 3 模型检测 2 3 1 模型检测概述 形式化验证可以用一种或多种( 规范) 语言来描述，这些语言包括命题逻辑、 一阶逻辑、高阶逻辑、时序逻辑、自动机、( 并发) 状态机、进程代数、耳一演算、 9 西北大学硕士学位论文 l l 一演算、特殊的程序语言，以及程序语言的子集等。 形式化验证主要包括两类方法，一类是以逻辑推理为基础的演绎验证 ( d e d u c t i v ev e r i f i c a t i o n ) ，另一类是以穷尽搜索为基础的模型检测( m o d e l c h e c k i n g ) 。 逻辑推理主要是定理证明，需要通过演绎推理证明软件的正确性，但推理 过程往往需要人工参与以使推理向正确的方向进行。这种方法对于稍微复杂的 系统，就使人为推理的过程十分繁琐，费时费力，效率较低。 模型检测( m o d e lc h e c k i n g ) “”是一种自动分析和验证的技术，是形式化验 证中很重要的一种方法。它是一种面向有穷状态并发系统的验证技术。其基本 思想就是状态搜索，它要求系统模型具有有穷状态空间。模型检测能够自动验 证一个系统是否满足其设计的规范，而且当规范不满足或检测出系统存在漏洞 时，模型检测工具能提供导致该结果的事件序列，从而为对系统进行漏洞定位 和系统的改进提供方便。 模型检测的基本思想是用状态迁移系统( s ) 表示系统的行为，用模态时序 逻辑公式( f ) 描述系统的性质，这样“系统是否具有所期望的性质”就转化为 数学问题“状态迁移系统s 是否是公式，的一个模型? ”，用公式表示为 sbf7 对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有 限时问内自动确定“”。如图2 1 所示。 图2 1 模型检测 对一个待验证系统进行模型检验一般要遵循以下步骤： ( 1 ) 建立模型把设计模型转化为模型检测工具所识别的形式化的模型。 有时因时间和空间资源的限制，要忽略一些细节性的东西，主要通过抽象或渐 进式建模策略来完成，以解决状态空间爆炸的问题。 ( 2 ) 性质描述给出要验证的系统的性质。性质可以用时序逻辑公式描 述，表示系统状态如何随时问而迁移。给出的性质应该是完整的，因为模型检 测只负责判断一个模型是否满足给定的性质，不考虑系统别的性质。 1 0 西北大学硕士学位论文 ( 3 ) 验证性质自动地进行验证。但实际应用中经常需要人的参与，主要 是对验证结果进行分析和总结。如果性质为假，模型检验工具要为用户显示出 导致性质为假的状态迁移路径，以用作待验证性质的反例。有时候由于建立的 模型的规模超出了现有计算机的正常处理能力，使得检验处于无穷运行或者死 机。这时候就要采取一些优化措施或者重新建模。 也就是说，模型检测是一个验证斗报错专错误信息分析和模型修改斗再 检测的循环过程。模型检测的基本过程如图2 2 所示： 图2 2 模型检测的基本过程 2 3 2 模型检测形式化描述方法分类 模型检测形式化描述与分析方法主要分成四大类：基于模型的形式化方法、 基于逻辑的方法、基于进程演算的方法以及基于网络的方法等等。实际上，很 多模型检测的形式化方法并不是采用单一的形式化技术，而是采取两种或多种 技术的综合应用。比如：在基于逻辑的方法中，采用p e t r i 网描述，而应用逻辑 进行推理等等。 基于模型的方法 基于模型的方法是通过构建一个数学模型支持系统的规范，给出系统的状 态和状态变换的显式操作。通常，一个规范描述一个系统的状态及其状态上的 操作，以及描述和下一个状态的关系。因此，特定的数学对象( 如数据结构、关 1 1 西北大学硕士学位论文 系或功能) 在结构上类似于详细描述的计算机软件需求，这些语言的语义是属于 集合论，在系统的整个设计过程和实现中，指定的数学对象在保留初始规范的 基本特征下是可调整的这样的规范语言代表是：v i e n n ad e v e l o p m e n t m e t h o d ( v d m ) “”和z 嘲概念。v d m 和z 是采用面向模型的方法，重点放在抽 象数据类型的描述上，抽象数据类型是通过公理来描述的，这些公理定义了抽 象数据类型上的操作之间的关系，它并没有给出类型的明确模型。 基于逻辑的方法 基于逻辑的方法主要用逻辑描述系统的特性，包括程序行为的低级规范和系 统时间的行为规范。在分布式系统形式化分析中，常用的逻辑模型检查方法主 要有：基于模态逻辑的方法。”、基于计算树逻辑c t l ( c o m p u t a t i o nt r e el o g i c ) 的方法蚴、基于时序逻辑x y z e 的方法嘲等。此外，还有一些基于逻辑的密码 协议形式描述与验证方法等。 基于进程演算的方法 基于进程演算的方法是给出系统并发行为模型，并通过进程的通信约束表 示行为，其核心通常是一种简单的语言，由带标号的变迁系统给出其操作语义。 当实现与规格说明都用该语言描述时，行为等效性建立了两者之间的联系，而 行为等效性则为系统验证及推导的复合提供了方便。进程演算的基本特点是建 立了并发系统潜在的不确定模型。通信顺序进程c s p ( c o m m u n i e a t i n gs e q u e n t i a l p r o c e s s ，c s p ) 、通信系统演算c c s ( c a l c u l u so f c o m m u n i c a t i n g ) 、靠演算等是进 程演算的代表“”，广泛用于并发系统的规格说明和验证。 通信顺序进程c s p 是1 9 7 8 年由c h o a m 提出的，试图提供一种在计算机 各个应用领域中广泛使用的简单数学模型。c s p 是很多并发分布式语言的思想 基础，是对并发程序设计语言的一次重要概念整理，它可看作是一种命令式程 序设计语言。c s p 模型实际上涉及了三个不同的抽象层次：规格说明、设计和 实现。 1 9 8 0 年r m i l n e r 提出的通信系统演算c c s ，其目标是将并发系统的语义理 论建立在通信基础上，它被看作为一种建立在极小原语集上的函数式程序设计 语言，研究并发系统的通信与不确定性提供了一个通用的数学模型。 c s p 和c c s 两种模型都基于相同的出发点，它们都将进程看作为构造系统 1 2 西北大学硕士学位论文 的基本构件，认为一个系统由若干进程构件通过各种方式( 选择、复合、隐藏等) 组合而成，而新形成的系统又可作为一个进程构件用于构造更大、更复杂的系 统。观察与同步通信是这两种模型的核心思想。演算是r m i l n e r 在c c s 模 型上发展起来的，其最大特点是允许进程之问将信道名字作为值来传递，从而 可描述通信拓扑结构可动态变化的并发系统，如移动电子商务系统等等。 基于网络的方法： 根据网络中的数据流，显式地给出系统的并发模型，包括网络中从一个结 点流向另一个结点的条件，如谓词变换网、p e t r i 网等。目前，p e t r i 网应用于分 析系统形式模拟与分析的方法很多。实际上，本章其他几节所涉及的某些形式 化方法，都是以p e t r i 网作为基本的形式化工具。p e t r i 网理论是在并发的概念上 建立起来的，它直观得表示了非确定性，可以用于表达不同抽象级上的系统概 念。p e t r i 网能用许多方法构造，例如简单c h a n n e l a g e n c y 网，用来表示系统结 构，在逐步求精后定义系统的行为；高级p e t r i 网提供划分系统方法，用另一种 方法表示系统结构。p e t r i 网通常表示为一种物理系统极为相近的图形形式，使 人们比较容易学习和理解。 本文所研究的模型检测形式化描述方法采用的是基于通信系统演算的方法 c c s ，即进程代数的方法。以下对系统模型的描述主要采用进程代数的方法。 在本文的第三章将有对进程代数的详细介绍。 2 4 模型检测中的状态空间爆炸问题 模型检测的主要困难是状态空间爆炸问题，即在把并发系统显式的表示为 状态迁移系统时，其状态数量随并发分量的增加呈指数增长。因此，当一个系 统的并发分量较多时，直接对其状态空间进行搜索在实际上是不可行的。状态 爆炸导致没有足够的空间和时间来分析状态迁移图是否满足性质，成了模型检 测在实际应用中的绊脚石。所以如何解决或者最大程度避免状态爆炸问题，成 了并发分布系统形式化验证的首要问题。 一般，显式的模型检测方法能够处理的系统状态个数可达1 0 8 伽。符号模 型检钡u ( s y m b o l i em o d e lc h e c k i n g ) 技术的出现使这一方法向实际应用性迈出了关 1 3 西北大学硕士学位论文 键的一步。其基本原理是用二叉 虱( b i n a r yd e c i s i o nd i a g r a m ) 表示状态( 集) 和状 态迁移关系，从而降低了系统模型所需的内存空间。符号模型检测方法能够 处理的系统状态个数可达1 0 1 5 0 叫嘲。 此外，为了减少模型检测所搜索的状态空间，还提出了“o n - t h e - f l y ”矧嘲、 偏序归约霉儿3 叮、对称模型检测1 蚴和抽象等技术剐。“o n - t h e - f l y ”技术的基 本思想是根据验证的需要逐渐展开系统状态，而不是事先构造完整的系统状态 空间。偏序归约和对称模型检测是为了避免重复验证，前者的出发点是独立并 发动作之间的任意交错是等价的，这样只须验证其中一种交错( i n t e r l e a v i n g ) 情形 即可，而后者则是基于进程间的对称性，即类似的进程可能产生许多相同或相 似的路径，这样只须验证在对称关系下等价的一种情形即可。抽象是解决复杂 问题的基本手段，包括对系统模型和性质的抽象。前者主要是通过简化或排除 细节，用尽量少的状态描述必要的系统模型；后者包括对要验证的性质进行分 解，降低公式的复杂程度等。本节在下文中详细介绍了目前提出的缓解状态爆 炸问题的这几种重要方法。 由于模型检测的基本思想是基于状态搜索的，搜索的可穷尽性要求系统模 型状态数有穷，故不能直接对无穷状态系统进行验证。因此对于一般软件来说， 首先需要有一个从任意状态到有限状态的建模过程。即使对于有穷状态系统， 模型检测也会面临“状态空间爆炸( s t a t es p a c ee x p l o s i o n ) ”的严重问题。 如何有效缓解“状态爆炸”是模型检测能被广泛使用的一个重要前提，在 这方面已有一些重要的方法被相继提出。西北大学网络与分布教研室也在此方 面做了很多工作，提出了基于假设的状态约减算法a b s r 嘲，在一定程度上解 决了组合状态爆炸问题，有效限制了并发系统模型的状态空间，并且设计