（计算机应用技术专业论文）反例引导的web应用模型检验.pdf

上海大学硕士学位论文 摘要 基于b s 模式的w e b 应用既保留了c s 模式分布计算的特性，又便于集中 管理，而且最重要的是对客户端的限制较少，因此极大地促进了w e b 应用的广 泛使用。w e b 应用已经对商业、工业、财政、教育、政府和娱乐及人们的工作 和生活产生了深远的影响。如何保证w e b 应用的正确性和可靠性得到业界的广 泛关注。 w e b 应用的验证是一个较新的研究领域，由于w e b 应用的异构、分布、并 发和平台无关等特性，使得对其验证比较困难。论文使用抽象技术来解决状态 爆炸问题，引入“反例引导的抽象精化”框架，试图实现模型检验的自动化。 首先，研究模型检验技术，考察时态逻辑公式的特点。使用接口自动机对 w e b 应用进行建模，通过接口自动机的组合来表达w e b 应用构件的组合。模型 检验器的验证结果表明组合模型在验证中的效率要优于未组合模型，但组合模 型有可能会存在状态空间爆炸问题。 其次，分析了状态爆炸问题，以及解决该问题的常见方法，给出了一种将 组合和抽象相结合的方法。改进了“反例引导的抽象精化 框架，针对多构件 w e b 应用，通过构造抽象模型的组合来构造组合模型的抽象。设计了抽象算法、 组合算法、转换规则、反例确认算法和抽象精化算法。 最后，根据设计的算法，开发了一个基于“反例引导的抽象精化”框架的、 图形化的w e b 应用模型检验辅助工具原型，自动解析用x m l 格式存储的模型 集和待验证的性质，完成抽象、组合、转换和验证等功能。当伪反例出现的时 候，自动进行抽象精化操作，并在控制台输出相应的验证信息，实现了w e b 应 用验证的自动化。 关键词：w e b 应用，模型检验，接口自动机，构件组合，反例引导的抽象 精化 上海大学硕士学位论文 a bs t r a c t w e ba p p l i c a t i o n ，w h i c hi sb a s e do nb sm o d e l ，n o to n l yp o s s e s s e st h ec h a r a c t e r i s t i c so f d i s t r i b u t e dc o m p u t i n go fc sm o d e l ，b u ta l s oc a nb em a n a g e dc o n c e n t r a t e l ya n de a s i l y , w h a t s m o r ei th a sn om o r er e s t r i c t i o nf o rt h eu s e r s ，t h u sd r a m a t i c a l l ym a k i n gt h ew i d ea p p l i c a t i o no f w e b w e ba p p l i c a t i o nh a sp r o f o u n d l yi n f l u e n c e do n rl i f ea n dw o r k ，s u c ha st h ee f f e c ti nt h e f o l l o w i n gf i e l d ：c o m m e r c e ，i n d u s t r y , f i n a n c e ，e d u c a t i o n ，g o v e r n m e n ta n de n t e r t a i n m e n t ，e t c s o ， m o r ea n dm o r ea t t e n t i o nh a sb e e np a i dt oc o r r e c ta n dr e l i a b l ew e ba p p l i c a t i o n v e r i f i c a t i o no fw e ba p p l i c a t i o ni san e wr e s e a r c hf i e l d i ti ss o m e w h a td i f f i c u l td u et ot h e f a c t o r so fi t sh e t e r o g e n e o u s n e s s ，d i s t r i b u t i o n ，c o n c u r r e n c y , p l a t f o r mi r r e l e v a n c y t h i sp a p e r e m p l o y st h ea b s t r a c tt e c h n o l o g yt os o l v et h ep r o b l e mo f “s t a t ee x p l o s i o n ”，i n t r o d u c i n gt h ef r a m e o f “c o u n t e r e x a m p l eg u i d e d a b s t r a c t r e f i n e m e n t ( c e g a r ) ”，a n d t h e n a c c o m p l i s h e s t h e a u t o m a t i z a t i o no ft h em o d e lc h e c k i n g f i r s t l y , m a k er e s e a r c ho nt e c h n o l o g yf o rm o d e lc h e c k i n g ，r e v i e wt h ef e a t u r e so fl t l m o d e lt h ew e ba p p l i c a t i o nb yu s i n gi n t e r f a c ea u t o m a t a ( i a ) ，a n du s et h ec o m p o s i t i o no fi at o e x p r e s st h ec o m p o s i t i o no fw e ba p p l i c a t i o n sc o m p o n e n t s t h er e s u l tg i v e nb ym o d e lc h e c k e r s h o w st h a tt h ec o m p o s e dm o d e li se f f e c t i v et h a nt h eu n c o m p o s e dm o d e l ，b u tt h ef o r m e rh a st h e p r o b l e mo f “s t a t ee x p l o s i o n s e c o n d l y , a n a l y z et h e “s t a t ee x p l o s i o n ，a sw e l la si t ss o l u t i o n s ，a n dt h e ng i v ean e w m e t h o dt h a ti n t e g r a t e sc o m p o s i t i o na n da b s t r a c t i o n i m p r o v et h ef r a m eo fc e g a kg e tt h e a b s t r a c t i o no ft h ec o m p o s e dm o d e lt h r o u g hb u i l d i n gt h ec o m p o s i t i o no ft h ea b s t r a c tm o d e l s ， r e s e a r c ha n dd e s i g nt h ea l g r o i t h m so fm o d e l sa b s t r a c t i o n ，c o m p o s i t i o n ，v e r i f i c a t i o na n d r e f i n e m e n t f i n a l l y , d e v e l o pap r o t o t y p eo fag u im o d e lc h e c k i n ga u x i l i a r yt o o lo fw e ba p p l i c a t i o n ， w h i c hi sb a s e do nt h ef r a m eo fc e g a r ，a u t o m a t i c a l l ya n a l y s e sm o d e ls e tw h i c ha r es t o r e di n x m lf o r ma n di t sf e a t u r e sw h i c hn e e d st ob ev e r i f i e d ，t h u sc o m p l e t i n gi t sf u n c t i o n sl i k e a b s t r a c t i o n ，c o m p o s i t i o n ，c o n v e r s i o na n dv e r i f i c a t i o ne t c w h e nc o u n t e re x a m p l ea r i s e s ，i tc a n a u t o m a t i c a l l yo p e r a t er e f i n e m e n t ，a n do u t p u t st h ec o r r e s p o n d i n gr e s u l to fv e r i f i c a t i o n ，r e a l i z e s t h ea u t o m a t i cv e r i f i c a t i o no f w e ba p p l i c a t i o n k e y w o r d s ： w e ba p p l i c a t i o n ，m o d e lc h e c k i n g ，i n t e r f a c ea u t o m a t a ，c o m p o n e n t c o m p o s i t i o n ，c o u n t e r e x a m p l eg u i d e da b s t r a c t i o nr e f i n e m e n t 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发表 或撰写过的研究成果。参与同一工作的其他同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示了谢意。 本论文使用授权说明 期固：墨： 本人完全了解上海大学有关保留、使用学位论文的规定，即：学 校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学校可 以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：靼导师签名：耻日期：掣 上海大学硕士学位论文 1 1选题背景和意义 第一章引言 i n t e m e t i n t r a n e t 以令人瞩目的速度快速发展，直接渗透到了社会的各个层面， 极大地促进了人类社会的发展。从1 9 8 9 年英国人t i m b e m e r s l e e 发明了万维网 ( w o r l d w i d e w e b ) 至l j 现在也不过2 0 年左右的时间，但是可以清楚的感受至u i n t e m e t 对我们的生活，对整个世界带来的翻天覆地的影响和改变。网上购物、电子商务、 数据传输，等等这些w e b 应用都在悄无声息地改变着我们传统的生活方式，各种 信息和数据可以在很短的时间内就传播到全世界。i n t e r n e t 的快速发展使“地球村 的概念变成现实，经济全球化在i n t e r n e t 的推动下日益流行。 随着网络通信技术的不断提高，许多传统的c l i e n t s e r v e r ( c s ) 应用程序正逐 步转向i n t e r n e t 上的w e bb r o w s e r w e bs e r v e r ( b s ) 模式。这一模式既保留了c s 模 式分布计算的特性，又便于集中管理，而且最重要的是对客户端的限制较少，只 需浏览器即可完成，这样极大地促进了b s 模式应用的广泛使用。如银行、政府 机构和在线商务企业都开始提供w e b 应用服务。w e b 应用也从初期的小型w e b s i t e 成功发展成了复杂的多层网络应用。w e b 应用程序可以同时分布在不同物理位置 为用户提供服务，其组成也由初期简单的h t m l 发展到现在种类繁多的多种技 术，l l , 女1 a s p ，j s p ，s e r v l e t ，n e t 等等。近年来，企业用户开始大规模采用w e b 应 用来提高生产和管理效率。w e b 应用逐步用于企业资源管理( e i u ) 和企业应用集 成( e a i ) ，而且它的成本低，使用方便，又是建立在工业标准基础之上。根据互 联网数据中- g , ( i n t e r n e td a t ac e n t e r , i d c ) 的预测，全球系统集成市场在2 0 0 5 2 0 0 9 年间的年复合增长率为4 6 ，2 0 0 9 年市场收入将达至1 j 8 9 9 亿美元 1 】。 在早期的w e b 应用的开发中，由于缺乏经验和严格的过程管理，开发人员在 w e b 应用的开发、发布、实施和维护的过程中，经常会遇到一些严重的问题，随 着w e b 应用变得越来越复杂，项目的开发和维护的代价逐步升级，很容易导致最 后的失败。同时，某些在c s 应用程序中简单而又容易处理的问题对w e b 应用开 发人员来说却是一个巨大的挑战。例如状态管理。由于b s 模式采用的是无连接 的h t t p 协议，在浏览器和w 曲服务器之间的h t t p 事务是独立的，无法保持一致 上海大学硕士学位论文 连续和连贯性的状态来跟踪用户的工作期。随着w e b 应用的广泛应用，各种漏洞 也逐渐滋生出来。如银行、政府等安全级别需求比较高的单位也都开始使用w e b 应用提供服务，这些机构往往自己开发整套的w e b 应用程序( a s p 、j s p 和c g i 等) ， 而由于早期的技术和经验的限制，导致这些软件存在许多漏洞。恶意用户可以查 看、修改或者插入敏感信息( 包括价格、会话跟踪等) ，s q l 注入、恶意脚本等 攻击方法层出不穷【2 1 。因此，w e b 应用的验证逐步引起了人们的关注。 w e b 应用与传统的应用软件( 比如c 程序，c s 模式应用) 有着许多不同的特 点，典型的w e b 应用由前端浏览器和后端服务器构成。前端通过各种浏览器、 脚本语言( j a v a s c d p t 等) 和a p p l e t s 等为用户提供复杂多元的图形化界面。后端包 括各种服务器网页文件( a s p 、j s p 等) 、c g i 程序、j a v as c r v l c t s 等，这些组成 部分又与其他跨平台的构件( c o m p o n e n t s ) 、数据库服务器和应用服务器进行交 互通信 3 1 。而用户可以使用不同的浏览器，采用不同的网络连接方式。 w e b 应用的异构性、动态性等特性使得对其验证非常困难。一些传统的验 证方法并不再适用于w c b 应用领域，因此，迫切需要有效的验证方法来保证w c b 应用的质量。w e b 应用的验证是一个较新的研究领域，相关研究还不多，因此 对w e b 应用验证方法的研究是一种新的挑战，这一研究不仅在学术上有重大的 意义，而且研究成果可以广泛应用到大量的w e b 应用开发过程中，具有广阔的 应用前景。 1 2w 曲应用验证的研究现状 w e b 应用的验证是一个较新的研究领域。近年来，一些相关研究相继开展 并取得了一定的成果。w e b 应用的形式化验证是从数学上证明w e b 应用是否实 现了设计人员的意图。这种验证通常需要采用某种形式化规约语言和逻辑构造 w 曲应用的模型，然后再验证该模型是否满足所给出的性质。 许多研究者提出或采用不同的模型，针对不同的系统提出了各种验证方法。 文献【4 】用接口自动机的组合运算对构件之间的交互兼容性进行检查，但没有对 系统行为是否满足某些需求规约进行检验。文献【5 】使用接口自动机和接口自动 机网络表示构件式系统的设计模型，使用u m l 顺序图表示基于场景的需求规 约，并对此模型与规约之间的存在一致性和强制存在一致性等性质进行分析， 2 上海大学硕士学位论文 给出了相关的验证算法。其它相关的研究还有：d o n i n i 等【6 】用一种扩展k _ r i p k e 结构一w 曲应用图描述w e b 应用的行为并给出了基于时态逻辑c t l 进行w e b 应用设计的性质检查方法。x l i 7 定义了u m l 序列图的静动态语义并提出了 检查序列图与u m l 其它模型如状态图等的一致性的方法。b u l t a n 8 】给出了一个 对w e b 服务组合的行为进行规约和验证的形式化框架，该框架用m e a l y 机为 w e b 服务的行为建模，用w e b 服务之间的会话来表达规约，通过自动机的组合 和包含关系进行验证。文献【9 】使用模型检验器s m v 对w e b 应用的行为与它的 设计的一致性进行了研究。h a y d a t 等用通信状态机为w e b 应用建模，提出了 一种从浏览器会话记录自动产生通信状态机的方法，该模型可以被用于w e b 应 用的性质验证和回归测试。但该文献没有给出性质的产生方法；d o n i n i 等使用 w e b 应用图w a g ( w e b a p p l i c a t i o n g r a p h ) 对窗体、网页以及网页中的连接和动 作进行形式建模以支持w e b 应用的验证 1 0 】，但该方法用于验证w e b 应用的设 计正确性而不是w e b 应用的具体实现，并且要验证的性质需要人为指定。 1 3 本文主要工作 论文的主要工作是开发一个针对w e b 应用的模型检验辅助工具原型，完成 w e b 应用模型检验的自动化。考虑到“状态爆炸 等问题，作者糅合了“反例 引导的抽象精化 【l l 】框架以及模型检验两种思想，使模型检验方法适用于构件 组合的w e b 应用模型。主要工作包括： 1 1w e b 应用构件的建模研究。由于w e b 应用异构性、动态性等特点，使 用何种方式对其进行建模便成了一个首要问题。采用接口自动机 ( i n t e r f a c ea u t o m a t a ) 1 2 】对w 曲应用建模，研究了接口自动机模型在模型 组合和抽象方面的优势和缺陷。 2 1 由于模型检验存在的“状态爆炸”问题，针对在组合模型时出现的问题， 引入“反例引导的抽象精化 框架，结合二者的优点，实现对构件组合 的w e b 应用的模型检验。 3 ) 模型检验辅助工具原型的设计与实现。设计了抽象、组合、验证与精化 等主要步骤的算法以及总体算法。实际开发了一个基于“反例引导的抽 象精化”框架的模型检验工具原型。 3 上海大学硕士学位论文 1 4章节安排 全文共分6 章： 第1 章主要介绍了本课题来源和w e b 应用的国内外研究现状，并阐述了作 者的主要工作。 第2 章介绍了w e b 应用形式化验证方法，并着重分析了模型检验方法以及 模型检验工具，最后引进反例引导的抽象精化框架，为后面的工作铺垫。 第3 章使用接口自动机作为w e b 应用建模工具，进行w e b 应用的模型检验， 阐述了模型检验的基本流程。 第4 章给出了解决状态爆炸问题的一种新的思路，将组合和抽象的思想结 合起来，糅合“反例引导的抽象精化框架，给出了对构件组合的w e b 应用进 行检验的方法。 第5 章在前一章节理论研究的基础上，设计了多个相关的算法，并基于该 算法开发了一个图形化检验工具。 第6 章总结本文的工作，并提出下一步继续研究的方向。 4 上海大学硕士学位论文 第二章w e b 应用验证概述 w e b 应用是用来完成某一任务的一系列相关的w e b 页面、技术与资源的集 合。与传统的c s 模式的应用程序通常采用一直保持连接的s o c k e t 安全套接字 协议不同，b s 模式的w e b 应用采用的是h 1 v r p 协议，这是一种无连接协议( 也 称作无状态协议) 。实际上，b s 模式的w e b 应用本质上也是一种c s 应用，只 不过w e b 应用采用浏览器作为客户端，在方便用户使用的同时将大部分业务转 移至服务器端，浏览器作为人机交互界面，服务器用于业务处理。w e b 应用服 务器端通常会由多层体系结构构成，在这种情况下，多层结构之间的通信以及 异构的多个构件之间的通信便很容易出现问题，严重影响了w e b 应用的质量及 安全。例如在2 0 0 5 年的上半年，中国大型在线书城一当当网发生的“缺货单 事件就给其带来了很大的损失，许多网民利用当当网订单系统的缺陷，免费获 得了许多商品，轰动一时。典型的w e b 应用具有分布式、异构性和动态性等特 点，这些特点对软件验证提出了新的要求，主要表现在w e b 应用的导航行为的 验证、构件组合验证等方面。因此对w e b 应用的验证进行研究是非常有必要的。 对w e b 应用的验证主要有两方面的工作，其一是对w e b 应用的代码进行检查， 查找错误和验证性质是否满足。其二是验证软件系统，把整个系统作为考察的 对象，对w e b 应用进行形式化建模和验证，这也是通常意义上的软件形式化验 证技术。 2 1形式化验证 形式化验证就是从数学上完备地证明系统是否实现了设计者的意图。这意 味着首先要用某种语言和逻辑构造系统的模型，然后运用严格的数学推理来证 明设计的正确性。形式化验证的主要优点是完备性，能够完全断定设计的正确 性。目前，主要的形式化验证方法有性质检验( p r o p e r t yc h e c k i n g ) 和等价性检验 ( e q u i v a l e n c ec h e c k i n g ) 1 3 1 ，其中性质检验又主要包括定理证明( m e o r e mp r o v i n g ) 和模型检验( m e d e lc h e c k i n g ) 两种。常见的形式化验证方法分类如图2 1 所示： 5 上海大学硕士学位论文 图2 1 形式化验证方法分类 等价性检验一般用于确保设计实现( i m p l e m e n t a t i o n ) 与设计规格说明 ( s p e c i f i c a t i o n ) 的一致性，它多用于硬件的底层设计之间的验证，如r t l 级、门 级和版图级之间的验证等。但它并不能确保设计规格说明的正确性j 此时就需 要用到性质检验。性质检验是指对一个实现方案，用形式化的方法检验它是否 满足某些规则或性质，它多用于高层，如行为级验证。性质检验包括定理证明 和模型检验。 定理证明通常使用公理和规则来验证设计实现是否满足要求。根据已构造 的系统规约抽取出反映系统应具有的性质，将其表示成定理，并加以证明，从 而达到对系统规约进行验证的目的。定理证明的一个主要缺点是不能完全自动 化，需要人工引导，能处理的设计规模较小，发展比较缓慢。 模型检验( m o d e lc h e c k i n g ) 是对有限状态并发系统( f i n i t e - s t a t ec o n c u r r e n t s y s t e m ) 的一种形式化确认方法，首先对系统建立一个有限状态模型，然后验证 所要求的性质在这个模型中是否满足。相比定理证明，模型检验的主要优点是 检验的自动化，在系统不满足性质时提供的反例路径可以用于诊断系统的错误， 因此比定理证明更受推崇。它的一个严重缺陷是“状态爆炸( s t a t ee x p l o s i o n ) p l 题 ，即随着所要检验的系统的规模增大，模型检验算法所需的时间空间开销 往往呈指数增长，极大限制了其实际使用范围。 2 2w 曲应用的形式化验证 我们知道，b s 模式的w e b 应用包括客户机和服务器两部分。因此，需要从 6 上海大学硕士学位论文 以下几个方面对w e b 应用一致性和安全性进行形式化验证【1 4 】： 1 1 导航行为的验证 网页是w e b 应用的图形界面，网页中的超链接或动作按钮为用户访问w e b 应用提供导航。导航行为的一致性要求w e b 应用实现了设计中的所有网页( 包括 静态网页和动态网页1 和连接，每个网页是可达的。同时，由于w e b 应用中通常 存在私密信息和受限功能，必须确保只有特定的授权用户才能访问私密网页和使 用受限功能。 验证导航行为的关键在于导航行为的建模和导航性质的产生。直观的导航模 型是一个以网页和软件构件为节点、以各种连接为边的有向图。为了应用模型检 验方法，一方面，需要根据网页的特性和连接事件产生导航行为的原子命题集， 用原子命题对导航行为的状态进行标记，建立导航行为的有限状态模型。另一方 面，需要根据w e b 应用的需求或设计自动生成导航性质。一般来讲，静态网页、 动态网页、软件构件以及不同的连接方式对应不同的原子命题、状态和性质。为 此，必须提供处理w e b 应用的连接多样性和动态性的建模规则和性质生成规则。 2 ) 构件组合行为的一致性验证 w e b 应用的服务器由诸如a s p 、j s p 、c g i 、j a v ab e a n 以及w e b 服务等多种 形式的构件组成，通过构件的组合提供业务逻辑和应用服务。这些构件的组合必 须相互兼容并且能满足业务逻辑的功能需求。 异构性、分布性和并行性增加了构件组合行为建模的复杂度。特别地，构件 组合所引起的组合状态爆炸问题使建立构件组合的全局状态空间非常困难甚至 不可能。因此，必须使用抽象、分层等模型归约技术以及组合推理、模型切片等 分解技术使验证在状态较少的抽象模型、单个构件模型或子系统模型上进行。 3 ) 构件组合行为的安全性验证 正常情况下，用户通过w e b 应用提供的导航使用w e b 应用，服务器的构件 组合应该提供导航所需要的接口。反之，导航也必须满足构件组合的安全性要求。 然而，与传统的客户机朋艮务器系统不同，w e b 应用的控制流程是可变的。 w e b 应用提供的导航只是用户使用服务器的一种方式。事实上，用户完全可以按 照自己的意愿改变导航行为，如编写自己的客户程序直接向服务器发送请求，也 就是说，构件组合的接口是开放的。利用构件组合的接口对系统实施攻击是一种 常用的攻击手段，构件组合的安全性至关重要。 7 上海大学硕士学位论文 2 3模型检验 模型检验是一种自动的、基于模型的、性质验证的方法，已经成功地被用 于许多实际问题中，包括硬件设计，协议设计，交互式系统分析等。 2 3 1 模型检验技术概述 模型检验方法首先由c l a r k e 和e m e r s o n 1 5 】于19 8 1 年提出，他们采用时态逻 辑表示系统的期望性质，用状态迁移图表示系统模型，通过对系统状态的搜索 来判断系统模型是否满足这些性质。模型检验是一种针对有限状态并发系统的 形式化自动验证技术。特别地，在并发或反应式系统中，并发相关的错误通常 不可再生或不被测试用例覆盖，通过测试方法很难发现，模型检验为检测这类 错误提供了一种有效的验证机制。 模型检验通常基于时态逻辑( t e m p o r a ll o g i c ) t 1 6 1 。时态逻辑可以很方便地表示 离散事件或状态是否发生以及发生的先后顺序，而在许多实际应用中人们不仅 关心某一事件是否发生，而且还要求它在确定的时间间隔内发生。这类对相关 事件发生的时间有明确要求的系统称为实时系统。由于实时系统涉及飞机控制 系统、机器人、工业以及军事控制系统等安全性至关紧要的应用领域，因此人 们对实时系统的模型检验非常关心，出现了许多表示实时系统的数字模型，比 如时间p e t r i 网、时间自动机、接口自动机及各种进程代数的时间扩充。时态逻 辑可以分为两大类：线性时间逻辑( l i n e a r - t i m el o g i c s ) 和分支时间逻辑 ( b r a n c h i n g - t i m el o g i c s ) 。1 9 8 1 年，p n u e l i 1 7 提出了线性时态逻辑l t l ( l i n e a r - t i m e t e m p o r a ll o g i c ) ，将时态逻辑引入到反应式程序的验证中。1 9 8 6 年，c l a r k e 、 e m e r s o n 和s i s t l a 1 s 提出了计算机树逻辑c t l ( c o m p u t a t i o nt r e el o g i c ) 。l t l 和 c t l 是模型检验最常用的两种时态逻辑，例如，模型检验工具s p i n t l 9 】使用l t l ， s m v 2 0 】同时支持c t l 和l t l 。与命题和谓词逻辑不同，时态逻辑公式涉及模 型中的多个状态，依赖于模型中的时间点，其真值可能发生动态变化。 随着研究的深入，更多种描述系统的时态逻辑被提出来，如a c t l ，c c t l ， e c t l ，p l t l 和p 演算的实时扩充，以及基于这些时态逻辑的各种算法研究和 规约研究。因此基于这些新的数学模型和时态逻辑，人们设计了各种新的模型 检验的算法，并实现了相应的分析与验证工具，如u p p a l l 2 l 】等。 模型检验技术的发展非常迅速，早期的模型检验侧重于硬件设计的验证。 上海大学硕士学位论文 随着研究的深入，模型检验的应用范围逐步扩大，涵盖了通讯协议、安全协议、 控制系统和一些软件的验证。人们通过对已有的统一建模语言u m l 的研究， 把u m l 状态机、实施活动图及顺序图等应用到模型检验中，从而可以直接利 用u m l 作为系统的建模工具，再转化为模型检验的状态迁移模型，进行相关 系统的验证。近年来，模型检验又有了一些新的发展和应用。如人们把模型检 验技术应用于非线性相似系统的验证，生成x m l 的搜索路径和分析系统的脆 弱性等等。随着信息技术和网络技术的发展，模型检验也开始被应用到w e b 应 用的程序设计、企业信息化及工作流控制等领域。通过验证和分析网络通讯协 议以及应用程序模型，提高企业信息化的稳定性和可靠性，形成高效的商业价 值。模型检验还被应用于化学过程验证和公司操作过程分析等方面。例如在化 学过程验证中，验证阀门，管道和容器的状况，将过程或系统抽象成一个有穷 状态模型，加以分析验证。 因为系统状态空间的有穷性，模型检验器可以通过对系统状态空间的遍历 判断公式是否成立。也就是说这个问题是可以判定的，在有穷的时间内是可以 完成的。而对于一些具有无限状态的系统，可以通过抽象和归纳规约到有穷状 态系统上。一次完整的模型检验通常分为三个步骤：系统建模、性质描述和工 具验证，如图2 2 所示： 图2 2 模型检验 其中： 系统建模。使用特定模型检验器的模型描述语言建立系统的形式模型。 在某些情况下，由于时空限制，需要进行抽象来消除无关或不重要的细 节。建模的方法有很多，比如u m l ，f s m 和自动机等，各种方法都有 各自的优点和不足。在第三章中我们尝试使用接口自动机对w e b 应用 进行了建模，并完成了基于接口自动机的w e b 应用验证。 9 上海大学硕士学位论文 性质描述。描述系统必须满足的性质，系统性质一般用时态逻辑描述。 三种最经常要验证的性质是：安全性( s a f e t y ) 、活性( 1 i v e n e s s ) 和公平性 ( f a i r n e s s ) 。安全性是指系统的正确性、互斥性和无死锁性，用于说明“坏 事情永远都不会发生；活性是指系统的终止性、无活死锁性、保证服 务性和响应性等，用于说明“好事情最终会发生 。公平性是指某事件 必须无限经常地发生。 工具验证。模型检验器以系统模型和性质( ) 作为输入，自动检验模 型是否满足给定的性质，即：检验m 户p ? 。模型检验将输出一个”y e s n o ” 式的检测结果。当性质不满足时，大部分模型检验器同时还会返回违背 性质的迹，即反例( c o u n t e re x a m p l e ) 。反例在错误诊断时非常重要。错 误可能是系统建模或性质不正确，但也可能是验证过程由于模型规模对 于计算机内存过大而失败终止。在后一种情况下，需要改变模型检验器 的参数或模型( 例如进行抽象) 后重新验证。 基于状态迁移系统的模型检验有两个重要的优点：一是建立在状态迁移系 统之上的模型检验是自动的，并且不需要用户掌握很深的数学方面的专业知识 就可以完成验证过程，这为模型检验的广泛应用提供了方便；二是如果系统模 型不满足某一指定性质，大部分的模型检验器都会给出相应的反例，标志错误 路径。这样的反例对查找错误和修正错误提供了非常有价值的帮助。 2 3 2 模型检验的缺陷及优化技术 模型检验方法的一个主要缺点就是“状态 爆炸问题。当系统的规模越来 越大时，模型检验所需要的空间和时间的开销将呈指数级增长，状态空间迅速 扩大，这样直接导致实际检验所需要的资源急剧膨胀。因此当一个系统的并发 分量或构件较多时，直接在其状态空间上进行搜索在实际上是不可行的。因此 为了能够有效地应用模型检验方法，需要研究减少和压缩状态空间。通过许多 研究人员的长期努力，一些方法已经得到实现。一方面，从扩充计算机处理能 力入手，用尽量少的资源处理尽可能多的状态。如：符号模型检验和o n t h e f l y 技术；另一方面，从限制系统模型的规模入手，尽可能压缩系统模型的状态， 使系统模型的状态空间缩d , n 可接受范围内。如：偏序规约、组合推理、程序 切片和抽象等。这样从一定程度上缓解了状态爆炸问题。 l o 上海大学硕上学位论文 符号模型检验( s y m b o l i cm o d e lc h e c k i n g ) 2 2 】的基本原理是将系统的状态转 换关系用布尔表达式表示。1 9 8 6 年，e r y a n t 将传统的b d d ( b i n a r yd e c i s i o n d i a g r a m ) 技术加以改进，使之成为布尔表达式的规范表示方法。m c m i l l a n 在 1 9 8 7 年将这种英语应用于模型检验中，并取得了巨大的成功。基于b d d 的模 型检验称为符号模型检验。在这种检验方法中，有序二叉图( o r d o r o db i n a r y d e c i s i o nd i a g r a m s ，o b b d ) 是用来表示布尔表达式的重要手段，它能较为紧凑地 表示状态转换关系，以降低系统模型所需要的内存空间。另外状态转换的计算 可以以集合为单位，提高搜索的效率。同样通过对迁移关系进行相应的不动点 运算可以得到要验证的时态逻辑公式的不动点的有序二叉图，进而可以用来分 析系统是否满足待验证的性质。符号模型检验并没有彻底地解决问题，其最大 瓶颈仍然是：存储和操作b d d 时对内存要求过大。b i e r e 等在1 9 9 9 年提出了 定界模型检验方法。定界模型检验是基于可满足。l 生( s a t i s f i a b i l i t y , s a t ) i h - 题的模 型检验，其主要思想是：在一个限定的步数k 内，考察系统运行的情况，确定 性质是否满足。若不能确定性质是否存在，则提高k 值，重新进行检验。s a t 问题虽然已证明是n p c o m p l e t e 问题，在实际应用中却很有效。 o n t h e f l ，2 3 】搜索技术的基本原理是根据需要展开系统路径所包含的状态， 这些状态只是搜索状态空间的一部分，这样可以避免生成系统中包含的所有状 态。o n t h e n y 搜索技术是一种局部模型检验技术，在构造系统全局模型( 多进 程构件模型的同步积) 的过程中检验性质的满足性，根据验证性质的需要展开系 统路径所包含的状态。这种方法的一个显而易见的优点是一旦验证算法找到一个 反例，算法即可终止，而不必生成剩余的状态空间，可以很好地解决内存不足和 状态爆炸等问题。 偏序归约( p a r t i a lo r d e rr e d u c t i o n ) 2 4 】技术是一种基于路径的状态化简技术。 一个系统通常可以由多个进程组成，在并发执行时不同进程的动作可以有不同的 次序，而一些不同的执行序列可能对于要验证的性质并没有本质上的差异。基于 这样一种认识，我们可以将某些状态的次序固定，减少重复验证本质上相同的路 径，使检验只针对所有可能执行路径集合中的一个子集。这种方法可以有效地缩 小待验证的状态空间的大小。对称模型检验技术( s y m m c r t r y ) 与此类似。 组合推理( c o m p o s i t i o n a lr e a s o n i n g ) t 2 5 】基于“分而治之的思想，利用系统的 组合结构对问题进行分解，通过检验各子系统的性质来综合推导出整个系统的 上海大学硕士学位论文 性质。组合推理策略主要有两种：简单组合和假设保证( a s s u m e g u a r a n t e e ，a g ) 组合。简单组合首先验证各子系统在任意环境下都满足的性质，然后从这些经 过验证的性质推出系统的整体性质。简单组合策略时没有考虑构件间的相互影 响，许多实际问题无法解决；a g 组合的思想是：为了验证m l 和m e 的并发组 合满足性质口八，先验证m 在任意环境都满足性质0 【，然后再验证m e 在任意 满足性质嘲环境下都满足性质。 程序切片【2 6 】是一种分析与理解程序的技术，通过程序系统依赖图提取出程 序中影响某个特定程序点变量值的语句集( 切片) 。该方法在程序调试中很有用， 得到的切片能够减小寻找错误和缺陷的范围。近年来，一些研究将程序切片技 术应用到模型检验。其主要思想是根据要验证的性质产生片标准，结合程序依 赖图产生程序切片，然后对程序切片进行模型检验，从而缩减模型检验所需的 状态空间。 抽象( a b s t r a c t ) 【2 7 】技术是缩小状态空间规模、避免空间爆炸的有效手段之一， 近年以来逐步得到了人们的关注。抽象的主要思想是通过将原始模型( 又称具体 模型) 的多个状态进行分组，得到一个保留了部分原始模型行为的规模更小的模 型，称之为抽象模型。为了保证验证工作的正确性，抽象模型必须满足一定的 条件，即强保持( s t r o n gp r e s e r v a t i o n ) ：抽象模型对于一个性质是强保持的，若性 质在抽象模型中为真，当且仅当该性质在原始模型中也为真。抽象技术的出现 和发展，有效改善了状态空间爆炸的问题，许多抽象方法涌现出来，比如谓词 抽象( p r e d i c a t ea b s t r a c t i o n ) 和局部抽象( l o c a l i z a t i o na b s t r a c t i o n ) 。但是即使有了 自动化模型抽取技术的支持，验证大型软件系统仍然是一个非常繁重的任务， 一个主要障碍是：抽象通常会引入具体模型不存在的附加的行为。当抽象模型 在检验中不满足性质，给出了相应的反例，我们不能肯定该反例一定存在于具 体模型中，因为这样的反例也有可能是在由于抽象而产生的。这样一种存在于 抽象模型但不存在具体模型的反例，我们称之为伪反例( s p u r i o u s c o u n t e r e x a m p l e ) 。由于伪反例的肯能存在性，因此当我们验证抽象模型出现反 例的时候，必须确定反例的真伪性，以用来确保之前的抽象模型是否需要修正， 这样的一个过程我们称之为抽象精化( a b s t r a c t i o nr e f i n e m e n t ) 。因此抽象、反例 确认和精化等几个过程的渐进发展，最终导致了“反例引导的抽象精化 1 2 上海大学硕士学位论文 ( c o u n t e r e x a m p l eg u i d e da b s t r a c t i o nr e f i n e m e n t ，c e g a r ) ”i l l l 框架的出现。本文的 主要工作也是基于这样一个框架，因此将在之后章节中详细介绍和使用它。 2 3 3 模型检验工具 相比较等价性检验和定理证明等其他形式化验证方法而言，模型检验方法 的一个非常重要的优点就是可以完全自动或半自动的进行验证，这一方法的成 功在很大程度上应归功于有效的软件工具的支持。按照验证对象的不同，大致 可以将这些模型检验工具分为两类：第一类是基于用户提供的模型。这些工具 往往需要采用特定的语言对待验证系统进行建模，比如s m v 和s p i n 等；第二 种是针对系统源代码验证。这类工具是随着对程序检验的需求不断扩大而出现 的，比如s l a m 2 8 1 、b l a s t t 2 9 1 、m a g i c 3 0 1 和v e r i s o f f 3 1 】等是c 程序的模型检验 工具；b a n d e r a 3 2 1 和j a v ap a t h f i n d e r ( j p f ) t 3 3 1 等是检测j a v a 程序的模型检验工具。 以下简要介绍几种知名的模型检验工具。 s s m v ( s y m b o l i cm o d e lv e r i f i e r ) 是由美国c a m e g i cm e l l o n 大学于1 9 9 2 年开发 的模型检验工具软件，用以检测一个有限状态系统是否满足c t l 公式。s m v 工具采用符号模型检验技术( s y m b o l i cm o d e lc h e c k i n g ) ，以二叉图表示状态的迁 移关系，