（计算机应用技术专业论文）web服务线性时态逻辑模型检查研究.pdf

摘要 由于应用的复杂性，在很多情况下单个w e b 服务难以满足实际需求，对于复 杂业务过程的处理需要采用服务组合的方法即由各个小粒度的w e b 服务相互之 间通信和协作来实现大粒度的服务功能。w e b 服务组合常用于描述跨组织的业务 流程等高层业务逻辑，这意味着系统的任何错误都可能导致严重的损失。保证服 务组合的正确性，确认服务组合的有效性是w e b 服务组合系统成功的关键。 本文将基于自动机的模型检查技术应用到w e b 服务组合中。首先从语义角度 研究了p r o m e l a 语义引擎问题。p r o m e l a 语言是模型检查工具s p i n 的核心，对 p r o m e l a 语言执行方式的理解决定所描述系统模型的行为方式。论文给出 p r o m e l a 语法的抽象对象模型的形式化定义和一个算法来实现p r o m e l a 语法到抽 象对象模型的映射，描述了p r o m e l a 指称语义。针对s p i n 中原子序列和同步通 信等复杂问题给出了解决方法。 然后提出了对基于w s - c d l 的w e b 服务组合的p r o m e l a 建模与验证。w s - c d l 支持的控制流机制包括：顺序、并发、同步、条件、非确定性选择等。论文提出 了一种w e b 服务数据流和控制流的模型，可以在数据流和控制流之间验证不利的 交互。w s c d l 进程模型的p r o m e l a 映射关键在于w s - c d l 进程模型验证相关方面 的确定以及如何执行这种映射。 最后利用模型检验工具s p i n 对有第三方支付平台参与的网上交易进行形式 化分析。实验证明此方案能够对基于w s - c d l 的w e b 服务组合进行行之有效的验 证。 关键词：w e b 服务；线性时态逻辑：形式化方法；模型检查 a b s t r a c t a s i n g l ea n ds i m p l ew e bs e r v i c e ( w s ) i sd i f f i c u l tt om e e tt h ea c t u a ld e m a n di n m a n yc a s e sd u et ot h ec o m p l e x i 够o fa p p l i c a t i o n s t od e a l 谢t l lt h ec o m p l e xb u s i n e s s p r o c e s s e si tn e e d st oc o m p o s ean u m b e ro fw s s an u m b e ro fw s so fs m a l lg r a n u l a r i t y c o m m u n i c a t ea n dc o l l a b o r a t ew i t l le a c ho t h e rt oa c h i e v ec o m p l e xs e r v i c ef u n c t i o n t h e c o m p o s i t i o no fw s si s u s e dt od e s c r i b et h ec o m b i n a t i o no fc r o s s o r g a n i z a t i o n a l b u s i n e s sp r o c e s s e s ，s u c ha sh i g h - l e v e lb u s i n e s sl o g i c ，w h i c hm e a n st h a ta n ys y s t e m e r r o r sc a i ll e a dt os e v e r el o s s e sa n df a u l t s t h ek e yt os u c c e s si st oe n s u r ea n dc o n f i r m t h ev a l i d i t yo fw e bs e r v i c e sc o m p o s i t i o n i nt h i s p a p e rm o d e lc h e c k i n g t e c h n o l o g yb a s e do na u t o m a t ai sa p p l i e dt o c o m p o s i t i o no fw s s f i r s t ，t h es e m a n t i co fp r o m e l ai ss t u d i e d p r o m e l al a n g u a g e i st h ec o r eo ft h es p i nt o o l ，t h eu n d e r s t a n d i n go fp r o m e l a i m p l e m e n t a t i o ni st h e d e c i s i o nt ot h eb e h a v i o ro ft h es y s t e m t h ef o r m a ld e f i n i t i o no ft h eo b j e c tm o d e lo f p r o m e l as y n t a xa n da na l g o r i t h ma r eg i v e nt oa c h i e v ep r o m e l aa b s t r a c ts y n t a xt o m a pt h eo b j e c tm o d e l ，d e s c r i b e st h ed e n o t a t i o n a ls e m a n t i c so fp r o m e l a t h e c o m p l e xi s s u e ss u c ha sa t o m i ca n ds y n c h r o n o u sc o m m u n i c a t i o na r eg i v e nt h es o l u t i o n t h e nf o r m a lm o d e l i n ga n dv e r i f i c a t i o nw i t hp r o m e l ab a s e do nt h ew s c d la r e p r o p o s e d t h ef l o wc o n t r o lm e c h a n i s m ss u p p o r t e db yw s - c d li n c l u d e s ：s e q u e n c e ， p a r a l l e l ，s y n c h r o n i z a t i o n ，n o n d e t e r m i n i s t i cc h o i c e ，e t e w ep r o p o s eam o d e l i n g p r o c e d u r et h a tp r e s e r v e st h ec o n t r o lf l o wa n dt h ed a t af l o wo fw s c d lp r o c e s sm o d e l s ， w h i c hc a l ld e t e c ti n c o r r e c ti n t e r a c t i o nb e t w e e nc o n t r o lf l o wa n dd a t af l o w t h em a p p i n g o fw s c d lt op r o m e l a h i n g e so nt h ed e c i s i o no fw h i c ha s p e c t so ft h ew s c d l p r o c e s sm o d e la r et o ( a n dc a n ) b ee x p r e s s e di np r o m e l a ，a n do nh o wt op e r f o r m s u c ham a p p i n g f i n a l l yu s i n gm o d e lc h e c k i n gt o o ls p i nt oa n a l y s i st h eo n l i n et r a d i n gw h i c h s u p p o r t e db yat h i r dp a r t y t h ee x p e r i m e n tp r o v e dt h a tt h ep r o c e d u r ec a nb ee f f e c t i v e f o rt h ev e r i f i c a t i o no fw e bs e r v i c e sb a s e do nt h ew s c d l k e y w o r d s ：w e bs e r v i c e s ；l i n e a rt e m p o r a ll o g i c ；f o r m a lm e t h o d s ； m o d e lc h e c k i n g 2 独创性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及 取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外， 论文中不包含其他人已经发表或撰写的研究成果，也不包含为获得江 西财经大学或其他教育机构的学位或证书所使用过的材料。与我一同 工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并 表示了谢意。 签名： 料隗 关于论文使用授权的说明 本人完全了解江西财经大学有关保留、使用学位论文的规定，即： 学校有权保留送交论文的复印件，允许论文被查阅和借阅；学校可以 公布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保 存论文。 ( 保密的论文在解密后遵守此规定) 签名：二蚪导师签名：继日期： 1 绪论 1 绪论 信息技术已经成为现代企业赖以生存和发展的基石，w e b 服务在现有的各种 异构平台的基础上构筑了一个通用的、平台无关的、语言无关的技术层，用来整 合异构信息孤岛。采用w e b 服务复合编排来实现业务流程对企业实现全球化和虚 拟化具有重要意义。本章介绍论文的研究背景、研究意义、研究现状和主要研究 内容。 1 1 研究背景 随着网络技术的不断发展，i n t e m e t 为各类型的商业实体提供了发现新客户、 供应流、新服务的各种机会，使他们利用i n t e m e t 获得了空前的、安全的经济回报， 体现了i n t e m e t 的巨大价值。但是人们发现在w e b 应用和传统桌面应用( 比如企业 内部系统、办公自动化系统等) 之间存在着连接的鸿沟，人们不得不重复地将数 据在w e b 应用和桌面应用之间迁移，这成为了阻碍w e b 应用进入主流工作流的一 个巨大障碍。计算机应用是要满足自动化的，在自动化流程之间的人工流程会在 不同程度上降低人们的积极性。i l j 各种不同的应用的开发语言不同，部署平台不同，通信协议也可能不同，对 外数据交换的格式也有着很大的差异。如何去解决语言差异、平台差异、协议差 异、数据差异所带来的高代价的系统集成是这个问题的关键。为了解决这类企业 或个人的不同平台之间的异构性，增强互操作性，w e b 服务1 2 j ( w e bs e r v i c e s ) 技 术应运而生。所谓“服务 指的是可提供某种功能的独立计算单元，允许其他人 调用以使用所提供的功能。w 曲服务位于i n t e m e t 上，可以是独立、无状态的业务 逻辑，也可能有更复杂的功能和接口，允许其他应用程序通过i n t e m e t 连接调用。 w 曲服务以s o a p 3 1 、w s d l 3 1 、u d d i 4 】等协议为核心，采用基于x m l 5 , 6 】的通信 的分布式软件组件的实现方式，屏蔽了底层消息传输协议和端点的消息处理等导 致传统软件组件异构的特征，屏蔽了异构平台的操作系统、网络类型和编程语言， 支持分布式环境中动态、开放的互操作模式，能很好地支持跨平台的应用。随着 w e b 服务概念的提出，互联网从单纯的数据提供者逐渐向服务提供者转型。 由于应用的复杂性，在很多情况下单个w e b 服务难以满足实际需求。对于复 杂的业务过程的处理，一般都采取服务组合的方法。w e b 服务组合1 7 j 是指：由各个 小粒度的w e b 服务相互之间通信和协作来实现大粒度的服务功能；通过有效地联 合各种不同功能的w e b 服务，服务开发者可以借此解决较为复杂的问题，实现增 值功能，比如常见的网上交易、企业订单服务等都是组合已有的组织内部的和组 织外部的服务来实现单个w e b 服务所不能完成的复杂功能。 w e b 服务线- j 生时态逻辑模型检查研究 由于w e b 服务组合系统中的各个w e b 服务可能是异构的、松耦合的、自主的， 存在着动态的交互关系，缺少中央控制( 有时也称为去中心的) ，而且，与一般应 用程序不同，w e b 服务组合常用于描述跨组织的业务流程等高层业务逻辑，这意 味着系统的任何错误都可能导致严重的损失保证服务组合的正确性。确认服务组 合的有效性是w e b 服务组合系统成功的关键，其重要性自不待言【8 】。所以我们必 须在w e b 服务组合实施之前检查w e b 服务组合流程的正确性、无死锁性等问题； 在w e b 服务被调用之前验证其与服务组合相容性的问题，如果不相容，需要重新 去发现符合需求的服务，然后再绑定执行【9 】。本文就是在此背景下提出的。本文将 基于自动机的模型检查技术应用到w e b 服务组合中，提出了对基于w s c d l 的 w e b 服务组合的p r o m e l a 形式化建模与验证，并用实验验证此方案能够对基于 w s - c d l 的w e b 服务组合进行行之有效的验证。 1 2 论文的研究意义 形式化方法( f o r m a lm e t h o d s ) 的基本含义是借助于数学的方法来研究计算机 科学中的有关问题。文献【1 0 】对形式化方法定义为：“用于开发计算机系统的形式化 方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架， 人们可以在该框架内以系统的方式刻画、开发和验证系统。 将形式化方法用于软件开发的主要目的是保证软件的正确性。形式化方法基 于严格的数学机制，而在软件开发过程中使用数学具有如下优点：数学是准确的 建模媒体，能够对现象、对象、动作等进行简短的、正确的描述；数学支持抽象， 它使得规格的本质可以被展示出来，并且还可以以一种有组织的方式来表示系统 规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格 中的矛盾和不完整性，以及用来展示设计和规格之间的一致情况等。 模型检型，1 2 1 是一种形式化验证技术，基于有限模型并检查该模型的期望特 性的一种技术，粗略地讲模型检查就是状态空间的蛮力搜索，模型的有限性确保 了搜索可以终止。将它引入到w e b 服务组合的验证，人们更好地理解w e b 服务组 合语言的基本机制，特别是探讨其中包含的新语言特性的本质。形式语义模型可 以提供对w e b 服务组合语言的推理基础，可以用语义模型来讨论给定的两个服务 组合的行为是否等价，判断某个服务组合是否是对另一个服务组合的扩展或抽象， 这是服务组合开发过程中常常需要考虑的问题。更直接的用处是，形式化分析技 术允许半自动( 基于定理证明技术) 或自动( 基于模型检查技术) 地检查服务组 合是否满足人们需要的各种性质，从而帮助消除设计缺陷，提高应用系统的可靠 性【13 1 。 将模型检查这一形式化方法用于w e b 服务的验证工作，将有助于： 2 1 绪论 ( 1 ) 更准确的描述w e b 服务的行为 ( 2 ) 更准确定义w e b 服务的特性 ( 3 ) 证明w e b 服务满足其特性说明，以及证明w e b 服务在什么条件不能满足 其说明 1 3 国内外的研究现状 模型检查技术已经在硬件系统、协议、软件系统的规格与分析中得到成功的 应用【1 4 - 1 6 1 。如何对w e b 服务进行形式化描述和验证是目前模型检查技术的一个重 要的研究方向。围绕w e b 服务组合的验证这个问题，已经有大量的研究者进行了 相当广泛和深入的研究，采用了不同的服务描述模型采用不同的模型检查方法， 检查不同类型的属性。 1 3 1 w e b 服务组合方法 单个的w e b 服务功能单一，很难满足实际需求。为了实现更复杂的业务逻辑， 就必须对w 曲服务进行组合。w e b 服务组合是指：由各个小粒度的w e b 服务相互 之间通信和协作来实现大粒度的服务功能；通过有效地联合各种不同功能的w e b 服务，服务开发者可以借此解决较为复杂的问题，实现增值功能。 服务组合主要包括以下作用1 1 7 j ： ( 1 ) 通过服务组合可以生成新的增值服务，使系统功能得到灵活扩展； ( 2 ) 复合服务对成员服务操作的调用是服务复用的一种体现，因此服务组合促 进了服务的复用； ( 3 ) 服务组合是一种控制复杂的手段。通过把小粒度服务组合成大粒度的、具 有业务含义的复合服务，可以使客户仅仅关心复合服务的接口和功能而不用考虑 复合服务的组成和结构，有效降低了客户使用系统的复杂性。 建立w e b 服务组合模型类似于业务过程建模，目前w e b 服务组合技术的标准 规范包括w s f l 1 8 ( w e bs e r v i c e f l o wl a n g u a g e ) 、x l a n g 1 8 ，1 9 1 、b p m l l 2 0 2 1 ( b u s i n e s sp r o c e s sm o d e l i n gl a n g u a g e ) 、w s c i 2 2 】( w e bs e r v i c ec h o r e o g r a p h y i m e r f a c e ) 、w s c d l 2 3 1 ( w e b s e r v i c e s c h o r e o g r a p h yd e s c r i p t i o nl a n g u a g e ) 和 b p e l 4 w s ( w e bs e r v i c e sb u s i n e s sp r o c e s se x e c u t i o nl a n g u a g e ) 等。当前在该研究方 向，规范正在趋于统一，主要存在如下三种技术：x l a n g 和w s f l 合并成为的 w e b 服务的业务流程执行语言( b p e l 4 w s b p e l ) ；业务流程建模语言( b u s i n e s s p r o c e s sm o d e l i n gl a n g u a g e ，b p m l ) ；w 3 c 的w e b 服务编排描述语言( w e bs e r v i c e s c h o r e o g r a p h yd e s c r i p t i o nl a n g u a g e ，w s - c d l ) 。 ( 1 ) b p e l 4 w s 2 4 】( b u s i n e s sp r o c e s se x e c u t i o nl a n g u a g ef o rw | e bs e r v i c e s ，w e b w e b 服务线性时态逻辑模型检查研究 服务商业流程执行语言) 是由i b m 、b e a 和m i c r o s o f t 共同推出w e b 服务的业务 过程执行语言。2 0 0 3 年4 月6 日交给o a s i s 组织审查并正式公布1 0 版本，并且成 立b p e l 4 w s 技术委员会，决定未来规范的发展方向。该委员会致力于产生一种用 于编写w e b 服务控制逻辑的，独立于平台的、基于x m l 的编程语言。2 0 0 3 年5 月 3 日由b e a 、i b m 、m i c r o s o f t ks a p 及s i e b e ls y s t e m s 五家公司完成b p e l 4 w s1 1 的版本。 b p e l 4 w s 是为组合w e bs e r v i c e s 而制定的规范标准。本质上来说，是i b m 公 司w s f l 和m i c r o s o f t 的x l a n g 的结合，w s f l 支持图形化的流程，微软的x l a n g 在结构化构造方面有独到的方法，b p e i a w s 吸取两者的优点，同时摒弃复杂繁琐 的部分，形成较为自然的描述业务流程的抽象程度较高的流程描述语言。 b p e l 4 w s 语言规范中没有任何与底层网络协议相关的部分，所有的信息传输都是 基于s o a p 协议来完成的。b p e l 4 w s1 。l 版本推出后，技术委员会又对b p e l 4 w s 1 1 做了大量的修改工作，使之得到全面的提高。随后推出w e b 服务业务流程执行 语言2 0 规范草案，把b p e l 4 w s 语言改称为w s b p e l ( w e bs e r v i c e sb u s i n e s s p r o c e s se x e c u t i o nl a n g u a g e ) 。根据网上公示得到的评论以及反馈回来的广泛的意 见，技术委员会又对w s b p e l 规范进行了进一步的修改。2 0 0 7 年1 月，w s b p e l 技术委员会把经过批准修改后的规范作为委员会草案，提交给o a s i s 组织，要求 批准成为正式的o a s i s 标准。 b p e l 4 w s 流程【2 4 】是一个流程图，用来表达特定业务的处理逻辑和算法，流程 的每一步称为一个活动。b p e l 4 w s 主要利用w s d l 使得服务的动态绑定成为可 能，但它没有提供具体方式来选取动态绑定时需要调用的服务，并且b p e l 4 w s 不支持在应用运行时的流程模型的调整。 ( 2 ) b p m l 2 4 ( b u s i n e s sp r o c e s sm o d e l i n gl a n g u a g e ) ，b p m l 是b p m i ( b u s i n e s sp r o c e s sm a n a g e m e n ti n i t i a t i v e ) 组织发布的规范。w f m c 和b p m i 在 2 0 0 2 年6 月2 6 日宣布将合作制定业务流程和工作流标准，即采用b p m l 来描述 工作流过程，同时采用x p d l 所定义的工作流模型。b p m l 规范的目标在于利用 业务流程管理系统的技术，促成标准的电子商务流程管理。其提供了一个表示业 务流程和支持实体的抽象模型，规范地描述了抽象并可执行的流程，该流程涉及了 企业业务流程的所有方面。b p m l 规范为表达业务流程和支持实体提供一个抽象 模型。b p m l 为表达抽象和执行流程定义了一种正式模型，该模型代表了企业业 务流程的面貌，包含了不断变化的复杂行为，事务和数据管理，合作，异常捕获， 操作语义。b p m l 为了能够持久化和通过异种系统进行定义交换以及使用建模工 具，提供了x m ls c h e m a 形式的语法。b p m l 从2 0 0 2 年1 1 月发布以后再没有较 大的进展。 4 1 绪论 ( 3 ) w s c d l 是由w 3 c 制定的用于描述w e b 服务编排的语言。该语言规范 目前是一份w 3 c 候选推荐标准( c a n d i d a t er e c o m m e n d a t i o n ) 。最新的版本是2 0 0 5 年1 1 月制定的。w s c d l 来源于p i c a l c u l u s ，抽象定义了交互信息的类型以及信 息交互的序列和条件，关注于可观察的服务与用户间的交互。一个编排描述指一 个多方的合约，从全局的视点描述多个客户间的客观可观察的行为。 1 3 2w e b 服务的模型检查 为了解决服务组合的这些问题，学术界和工业界提出了多种方法，总体来说， 其思路可以分为三类：基于自动机理论、基于p e t r i 网理论和基于进程代数。 在采用模型检查技术对w e b 服务进行验证的过程中，首先要选择相应的w e b 服务描述模型并选择合适的模型检查器，将现有的w e b 服务的过程描述模型转化 为m o d e lc h e c k e r 能够接受的描述形式；接着设定待检查属性的描述方法，并且保 证这种表示形式也能够被模型检查器识别，最终由m o d e lc h e c k e r 通过相应算法对 组合服务及其原子服务进行检查，根据其是否满足待检查属性，得出检查结果以 及检查报告。 ( 1 ) 基于自动机【2 5 j 自动机【2 q ( a u t o m a t a ) 或者标记迁移系统【2 7 】( 1 a b e l e dt r a n s i t i o ns y s t e m s ，l t s ) 是一种著名的用于系统行为建模的基本的形式模型。由于状态机本质上的可操作 性因而它成为多种操作模型的基础。许多基于自动机的形式化模型比如i o 自动机 2 8 1 、时间自动机2 9 1 、队列自动机3 川等被用来对对w 曲服务进行形式化描述、复合 和验证。 美国加州大学的开发人员提出的w s a t 3 1 , 3 2 l ( w e bs e r v i c e a n a l y s i s t 0 0 1 ) 。该系 统采用s p i n 作为检查工具，对基于b p e l 定义的、通过异步x m l 消息交互的组合 w e b 服务及服务间的交互活动进行形式化描述，在w s a t 中，首先将w e b 服务描述 模型( 例如b p e l 4 w s 等) 转换为w s a t 的模型语言g u a r d e da u t o m a t a , 进而转换为 s p i n 的输入语言p r o m e l a 进行检查。作为一种中间转换语言，g u a r d e da u t o m a t a 用来描述模型的交互，交互活动可以由一组状态集合和改变状态的行为集合表示。 该系统提出的模型中，待检查属性用l t l 来表示，给定一个组合w e b 服务s 和一 个l t l 表示的属性，通过设定相应的属性，来分析组合w e b 服务是否满足这些性质， 从而达到验证w e b 服务的目的。 ： n a k a j i m as h i n 等人提出利用s p i n 作为验证工具验证基于w s f l 的组合 w e b 服务，w s f l 它描述了服务组合过程中各个服务间的控制流和数据流。验证 过程是将w s f l 描述转化成s p i n 的形式化描述语言p r o m e l a ，应用程序待检查 属性包括各服务节点的可达性、服务流无死锁及应用程序中的特定过程属性等， w e b 服务线- 性时态逻辑模型检查研究 由l t l ( l i n e a rt e m p o r a ll o g i c ) 公式描述，也被输入到s p i n 中，s p i n 接受p r o m e l a 和l t l 两种互补的描述信息，通过求二者的交集是否为空来判断系统是否满足特 定属性。该方法较好检查了服务在运行前服务流描述规范中的错误，保证了w e b 服务组合过程的正确执行。 ( 2 ) 基于p e t r i 双j 2 5 , 3 3 1 ： p e t r i 网是一个适合于研究具有并发竞争同步等特征行为的形式化技术，常用 来描述并发异步活动的系统模型，它有4 种基本元素：位置、变迁、弧和权标。 位置表示系统可能进入的当前状态；变迁由水平线或者竖线表示，每个变迁具有 从输入位置来的0 个或者多个输入弧和到输出位置的1 个或者多个输出弧。如果 一个变迁的每个输入位置都至少有一个输入权标，则该变迁就能被使能。 p e t r i 网模型用于提供一种形式化的表示顺序、并发概念以及标识和解决歧义 性的方法。它是规范和验证通讯协议的一种有效工具。该模型虽然能够用于精确 的说明顺序、并发和同步等概念并能够很好地定义和解决并发系统中很多性质， 如正确性、无死锁性、互斥等，但用于描述并发系统时存在两个缺陷：首先并不 具有层次结构；其次，它只能说明系统的控制流而不能说明系统的数据流。 斯坦福大学的s r i n in a r a y a n a n 等人，采用p e t r i 网理论研究了o w l s 的操作 语义，他们首先研究了原子服务描述与情景演算之间的转换关系，即用情景演算 理论研究了o w l s 中原子服务描述的形式语义；在此基础上，将情景演算作为中 间语言，通过把情景演算转换为p e t r i 网，然后用p e t r i 网的理论来研究了语义w e b 服务的执行推理，即语义w e b 服务的操作语义。 ( 3 ) 基于进程代数1 2 5 ，3 3 j c s p 3 4 ，3 5 】模型是h o a r 仓o 立一种适用于计算应用领域的最简单的数学理论模 型。虽然这种模型能把计算机所涉及的各种计算形式及其性质用一套严密的形式 系统来模拟，但是它以进程中事件的顺序执行及进程间通讯为出发点来研究并行 计算的一般模式。因此，其并行计算的能力有限。 c c s t 3 5 , 3 6 1 系统是米勒( m i n l e r ) 在上世纪七八十年代提出的一种进程代数系统， 它用代数的方法着重刻画交互式系统的并发行为。它捕获了并发性及通讯的一般 代数性质而成为一个能有效描述并发系统功能的代数模型。c c s 模型它第一次提 出了将计算建立在通讯机制上，是真正“并发意义上的计算模型。与以往的并 行计算模型相比，它并行计算能力强，概念简单、清晰，表达和推理能力很强， 它提出了建立在互模拟基础上的可观测等价。 p i 演算是对c c s 的扩展，它是由m i l n e r 、p a r r o w 和w a l k e 在e n g b e r g 和n i e l s e n 工作的基础上提出的。它扩展了c c s 的并发计算能力。此模型忽略了c c s 中的通 道和变量的差别而将它们统一为名，所以它的基本计算实体只有名和进程，进程 6 1 绪论 之间的通信是通过传递名来完成的。由于可以传递通道名，因此p i 演算具有了建 立新通道的能力，所以p i 演算可以用来描述结构不断变化的并发系统( 即系统中 进程之间的连接关系可随着进程状态的不断变化而发生改变) 。与c c s 不同，它是 一个封闭的计算模型。可用于描述结构动态可变的系统。 ： b r o g i ，c a n a l ，p i m e n t e l 等提出了一个基于c c s ( c a l c u l u so fc o m m u n i c a t i n g s y s t e m s ) 的w e b 服务编排接口( w 曲s e r v i c ec h o r e o g r a p h yi n t e r f a c e ，w s c d 的形式 化模型。 电子科技大学计算机科学与工程学院的廖军、谭浩和刘锦德，提出了基于p i 演算的w 曲服务组合的形式化描述和验证，文献【7 j 讨论了p i 演算与w e b 服务协议 栈的对应关系，说明了利用p i 演算建立w e b 服务组合模型的规则，指出了如何寻找 代理和通道。最后建立了服务组合的p i 演算模型。在m w b ( m o b i l i t yw o r k b e n c h ) 模型检查工具的支持下，对组合服务进行推演和验证。 在现实世界的场景中，企业或者组织通常不愿意把对自己业务过程的控制权 委托给它们的集成合作方。编排的思想提供了一种途径，通过它各个实体可能以 合作方式共同定义出一套清晰的参与规则，而后各自根据公共全局观点确定的编 排实现其中自己的那个部分。w s c d l 中还希望表述这些实现与其公共观点的相 符性，使之能够方便地检查。采用w s c d l 规范做出的一个合约是一个有关信息 交换的公共顺序性条件和约束的”全局”定义，它以全局观点描述了所有参与方的公 共的和互补的可观察行为。各个参与方可以根据这一全局定义构造和测试与之相 符的解决方案。该全局规范转而由这样得到的局部系统的组合在适当基础设施的 支持下实现。 基于w s c d l 的w e b 服务的模型检查的研究还只是刚刚起步，已有的研究方 法主要采用基于进程代数的方法，而基于自动机理论的方法还没有开展。本文拟 借助于成熟的基于自动机理论的模型检查工具s p i n 对基于w s c d l 的w e b 服务 进行形式化建模与验证，从而确保w e b 服务的正确性。 1 4 本文的主要研究内容 研究方案采用模型检查技术验证w e b 服务的相关协议和描述，主要是将用 w e b 服务建模语言w s c d l 建立的w e b 服务模型转换成为形式化的有限状态机模 型，并将其属性用线性时态逻辑l t l 表示，借助模型检查工具s p i n 对w e b 服务 的活性、安全性、公平性和是否死锁等特性【3 7 】进行验证和确认。 具体包括： ( 1 ) s p i n 语义模型研究 s p i n 的工作原理；p r o m e l a 的语义引擎执行方式 7 w e b 服务线性时态逻辑模型检查研究 ( 2 ) w 曲服务的建模方法 对系统进行模型检查的过程中，建模技术是关键的技术之一。模型检查的第 一步是对实际系统进行形式化建模，去除与验证属性无关的细节，并将服务规范 用形式化方法描述。运用抽象技术去除w e b 服务中与验证属性无关的细节，建立 w e b 服务的形式化模型。 ( 3 ) w e b 服务的特性描述方法 运用线性时态逻辑l t l 刻画w e b 服务的特性，例如活性( 1 i v e n e s s ) 、安全性 ( s a f e t y ) 、公平性( f a i r n e s s ) 和有无死锁( d e a dl o c k ) 。 ( 4 ) 基于s p i n 的模型检查方法 运行模型检查工具s p i n 对w e b 服务实例进行模型检查并分析验证结果 1 5 论文的结构安排 本文的组织结构如下：第2 章介绍w e b 服务和模型检查；第3 、4 章为本文的 重点，也是本文的主要贡献所在，第3 章主要研究了p r o m e l a 语义模型及 p r o m e l a 语句到语义模型的映射算法；第4 章介绍了w e b 服务编排的建模与分 析；第5 章对有第三方支付平台参与的网上交易过程进行形式化建模与特性验证； 最后，第6 章总结全文，并对未来的工作进行展望。 8 2 理论基础 2 理论基础 将模型检查这种可信且强大的系统自动验证技术应用在w e b 服务复合的有 效性验证上，可以检查服务组合是否满足人们需要的各种性质，从而帮助消除设 计缺陷，提高应用系统的可靠性。本章介绍w e b 服务及模型检查相关理论。 2 1w e b 服务 2 。1 1w e b 服务的基本概念 一般来说，w e b 服务是由u r i 标识的软件系统，w e b 服务作为一种特殊的 服务继承了服务的自治性、开放性、自描述性和实现无关性，同时w e b 服务是 通过i n t e m e t 实现远程访问的。下面是w 3 c 对w e b 服务的定义。 w e b 服务：是由u r i 标识的软件应用，其接口和绑定可以用x m l 来定义和 描述并且可以被发现，与其他软件通过i n t e m e t 的协议以x m l 消息交换的方式 直接交互。 w r e b 服务是用标准的、规范的基于x m l 的w s d l 语言描述的，这称之为 w e bs e r v i c e s 的服务描述。这一描述囊括了与服务交互所需要的全部细节，包括 消息格式、传输协议和位置。该接口隐藏了服务实现的细节，允许通过独立于服 务实现、独立于硬件和软件平台、独立于编写服务所用的编程语言的方式使用该 服务。 2 1 2w e b 对象 从外部使用者的角度而言，w e b 服务是一种部署在w e b 上的对象组件，它 具备如下特征3 引。 完好的封装性：w e b 服务是部署在w e b 上的一种对象或组件，具有良好的 对象封装性，使用者能且仅能看到该对象提供的功能列表。 松散藕合：当w e b 服务的调用界面保持一致时，w e b 服务的实现变更对调 用者是完全透明的。w e b 服务通过x m l s o a p 作为消息交换协议保持其松散耦 合。作为w e b 服务，其所有公共的协约需要使用完全开放的标准协议进行描述、 传输和交换。这些标准协议具有完全免费的规范，以便由任意方实现一般而言， 绝大多数规范将最终由w 3 c 或o a s i s 作为标准版本的发布方和维护方。 高度可集成能力：由于w e b 服务采取简单的、易理解的标准w e b 协议作为 组件界面描述和协同描述规范，完全屏蔽了不同软件平台的差异，无论是 c o r b a 、d c o m 还是e j b ( e n t e r p r i s ej a v ab e a n s ) 都可以通过这种标准的协议进行 互操作，实现了当前环境下最高的可集成性。 9 w e b 服务线性时态逻辑模型检查研究 2 1 3w e b 服务不同角度的描述 w e b 服务具有广泛的适应性和应用背景，而且w e b 服务的很多相关问题仍 处在研究过程中，我们可以从不同的侧面对w r e b 服务有不同的描述。p 州 ( 1 ) 从功能的角度描述w e b 服务，认为w e b 服务基于t c p i p 、h t t p 、x m l 等规范而定义，具备如下功能：w e b 上链接文档的浏览、事务的自动调用、服务 的动态发现和发布。 ( 2 ) 从组成框架及实现目标的角度描述了w e b 服务，认为w 曲服务作为一 种网络操作，能够利用标准的w e b 协议及接口进行应用间的交互。 ( 3 ) 从语义的角度描述了基于语义w e b 的服务，认为w e b 服务是语义w e b 的一种应用，由于考虑了语义信息的描述及表示，w e b 服务能够更准确地被执行， 服务组合( s e r v i c ec o m p o s i t i o n ) 能够按所期望的目标进行。 ( 4 ) 从网格计算( g r i dc o m p u t i n g ) 的角度指出w e b 服务能用于w r e b 上的资源 发现、数据管理及网格计算平台上异构系统的协同设计，提出了网格服务的新概 念。 ( 5 ) 从信息检索的角度提出了在包含了分布策略和路由信息的电子文档之 上进行分布式文档检索的w 曲服务。 2 1 4w e b 服务的体系架构模型 w e b 服务体系结构基于三种角色( 服务请求者、服务提供者和服务注册中心) 之间的交互。交互涉及到发布、查找和绑定操作。图2 1 展示了这些操作、提供 这些操作的组件以及他们之间的交互l l j 。 ( 1 ) 角色 w e b 服务体系结构中的角色如下： 服务请求者( s e r v i c er e q u e s t e r ) ：也经常被称为服务使用者。从体系结构的 角度看，这是寻找并调用服务或启动与服务交互的应用程序、软件模块或需要服 务的另一种服务。它发起对注册中心服务的查询，通过传输绑定服务，并执行服 务功能，服务使用者根据接口契约来执行服务。 服务提供者( s e r v i c ep r o v i d e r ) ：它是一个可通过网络寻址的实体，接收和 执行来自使用者的请求。将自己的服务和接口契约发布到服务注册中心，以便服 务使用者发现和访问该服务。 服务注册中一t 二, ( s e r v i c er e g i s t r y ) ：也经常被称为服务代理。这是可搜索的服 务描述注册中心，服务提供者在此发布他们的服务描述。在静态绑定开发或动态 绑定执行期间，服务请求者查找服务并获得服务的绑定信息( 在服务描述中) 。 1 0 2 理论基础 图2 1w e b 服务体系结构 ( 2 ) 行为 w e b 服务体系结构中的每个实体都扮演着服务提供者、使用者和注册中心这 三种角色中的某一种( 或多种) ，它们必须执行以下三个行为：发布服务描述、 查询或查找服务描述、根据服务描述绑定或调用服务。 发布( p u b l i s h ) 为了使服务可访问，需要发布服务描述以使服务使用者发现和 调用它。 发现( f i n d ) 服务请求者直接检索服务描述或在服务注册中心来查找满足其需 求的服务。 绑定( b i n d ) ：检索完服务描述之后，服务使用者根据服务描述信息定位、联系 和调用服务，从而在运行期间调用或者启动与服务的交互。 ( 3 ) w e b 服务协议栈n 7 1 w e b 服务体系由一系列开放的协议和规范组成，这些协议和规范可以由任意 方式实现。为了标准化w e b 服务技术，w 3 c 和o a s i s 都成立了相应的工作组进 行w e b 服务的标准化工作。i b m 、微软、h p 、s u n 、o r a c l e 等公司也在积极促 进w e b 服务技术的发展和标准化。w e b 服务协议栈如图2 2 所示。 传输规范 传输协议提供基本的数据传输服务，w e b 服务可以利用多种网络协议实现 x m l 消息的传递，h t t p ( h y p e r t e x tt r a n s f e rp r o t o c 0 1 ) 作为一种使用最广泛的 w e b 通信协议是w e b 服务的首选，w e b 服务可以通过基本的h t t p 操作 ( g e t p o s 聊u t d e l e t e 等) 发送x m l 消息。其它可利用的传输协议包括 s