（计算机软件与理论专业论文）web服务组合形式化验证和服务选择算法研究.pdf

浙江大学硕士学位论文摘要 摘要 w e b 服务为企业i t 体系结构带来互操作性、灵活性和复用性，改变了商业伙 伴之间的合作方式，使企业能通过服务组合来共享资源，自动化商业流程。w e b 服务组合问题近年来成为研究热点。 基于服务编排和编制的组合方法的结合能够有效提高服务流程建模的效率 和准确性，w s - c d l 、w s - b p e l 分别是基于服务编排和编制的主要组合规范。但二 者属于不同层次的技术规范体系，其针对服务流程描述的一致性需得到保证。二 者的一致性验证是个亟待研究的问题。 随着w e b 服务种类和数量的不断扩大，面向服务组合规模较大背景下的服务 选择立刻凸现，其中服务选择的算法是核心问题。但目前已有工作很少涉及到此。 针对上述问题，本文研究成果体现在以下两个方面： 1 ) 基于c s p 的w e b 服务编排和编制一致性检查。在设定的转化规则下，w e b 服务编排语言w s c d l 和w e b 服务编制语言w s b p e l 被映射为c s p 语言， 然后基于c s p 的模型检测工具p a t 将进行二者的一致性检测。并给出了 一个电子商务的案例。 2 ) 提出大规模w e b 服务选择算法g a e l s 。针对候选服务众多的大规模w e b 服务选择问题，提出一种新的w e b 服务选择算法g a e l s ( g e n e t i c a l g o r i t h me m b e d d e dl o c a ls e a r c h i n g ) ，该算法运用高适应度初始种群 和局部搜索的变异策略，加快收敛速度。通过实验评测表明与简单遗传 算法相比，g a e l s 算法能更快得到近似最优解，且随着服务规模增长， 拥有更好的适应性。 关键词：w e b 服务组合，服务编排，服务编制，一致性验证，服务选择算法 浙江人学硕二t 学位论文a b s t r a c t a b s t r a c t w e bs e r v i c e sm a k et h ee n t e r p r i s ei ta r c h i t e c t u r em o r ep o w e r f u li ni n t e r o p e r a b i l i t y , f l e x i b i l i t ya n dr e u s a b i l i t y i na d d i t i o n ，t h ec o o p e r a t i o nm e t h o d sb e t w e e nc o m m e r c i a l p a r t n e r s a r ec h a n g e db yu s i n gw e bs e r v i c e si ns o m es e n s e t h r o u g hs e r v i c e s c o m p o s i t i o n ，c o m p a n i e sc o u l ds h a r er e s o u r c e sa n da u t o m a t eb u s i n e s sf l o w s ow e b s e r v i c e sc o m p o s i t i o nr e s e a r c hi sb e c o m i n gah o ta r e ad u r i n gt h e s ey e a r s c o n j u n c t i o no fs e r v i c e sc h o r e o g r a p h ya n ds e r v i c e so r c h e s t r a t i o nc o u l de n h a n c e e f f i c i e n c ya n dv e r a c i t yo ft h eb u s i n e s sp r o c e s sm o d e l i n gg r e a t l y w s b p e la n d w s c d la l et h em a i ns e r v i c e sc o m p o s i t i o ns p e c i f i c a t i o n st h a tb a s e do ns e r v i c e s c h o r e o g r a p h ya n ds e r v i c e so r c h e s t r a t i o nr e s p e c t i v e l y h o w e v e r , s i n c et h e yb e l o n gt o d i f f e r e n tt e c h n i c a ls p e c i f i c a t i o nl e v e l s ，i ti sb e t t e rt om a i n t a i nt h ec o n s i s t e n c yo ft h e i r b e h a v i o r s h o wt ov e r i f yc o n s i s t e n c yo fs e r v i c e sc h o r e o g r a p h sa n do r c h e s t r a t i o ni sa p r o b l e mn e e dt ob es o l v e d a sm o r ea n dm o r ew e bs e r v i c e sa r ed e v e l o p e d ，t h ei s s u el a r g e - s c a l ew e bs e r v i c e s s e l e c t i o nh a sm o r ew e i g h tt h a nb e f o r e t h ek e y p o i n to ft h i si s s u ei sh o w t op r o p o s ea n e f f i c i e n ta l g o r i t h mf o rt h i si s s u e h o w e v e r , m o s tw o r ko nh a n dh a sn o ta d d r e s s e dt h i s t os o l v et h ep r o b l e ma b o v e ，p o i n t so ft h et h e s i sa r em a i n l yo nt h ef o l l o w i n g ： 1 ) c s p b a s e dv e r i f i c a t i o nf o rs e r v i c e sc h o r e o g r a p h ya n ds e r v i c e so r c h e s t r a t i o n a c c o r d i n gt ot h et r a n s l a t i o nr u l e sp r o p o s e d ，b o t hw s c d la n dw s b p e la r e m a p p i n gi n t oc s pl a n g u a g e ，t h e nm o d e lc h e c k i n gt o o lp a t , w h i c hi sb a s e do n c s p , c h e c kt h ec o n s i s t e n c y w ew i l lg i v ea ne - b u s i n e s sc a s ei no u rp a p e r 2 ) a ne f f i c i e n ta l g o r i t h mg a e l sp r o p o s e df o rl a r g e - s c a l ew e bs e r v i c e ss e l e c t i o n a i m i n gt os e r v i c es e l e c t i o np r o b l e mw i t hm a s sc a n d i d a t e s ，w ep r o p o s ean e w a l g o r i t h mn a m e dg a e l s ( g e n e t i ca l g o r i t h me m b e d d e dl o c a ls e a r c h i n g ) ，w h i c h u s e st h es t r a t e g i e so fh i g h f i t n e s si n i t i a lp o p u l a t i o na n dm u t a t i o nw i t hl o c a l s e a r c h i n gt os p e e dt h ec o n v e r g e n c e t h ei n d e p t he x p e r i m e n t a lr e s u l t ss h o wt h a t t h ep r o p o s e da l g o r i t h mg a e l sc a ng e tt h ea p p r o x i m a t e l yo p t i m a ls o l u t i o nm o r e q u i c k l ya n db em o r ea d a p t i v et ot h ee x p a n d i n go fc a n d i d a t es e r v i c e st h a ns i m p l e 浙江大学硕士学位论文 a b s t r a c t g e n e t i ca l g o r i t h m k e y w o r d s ： w e bs e r v i c e sc o m p o s i t i o n ，s e r v i c e sc h o r e o g r a p h y , s e r v i c e so r c h e s t r a t i o n ， c o n s i s t e n c yv e r i f i c a t i o n ，s e r v i c e ss e l e c t i o na l g o r i t h m 浙江大学硕士学位论文图目录 图目录 w 曲服务体系结构6 w 曲服务规范协议栈7 w 曲服务一致性检测流程1 9 w s c d l 主要元素层次关系2 0 w s b p e l 主要元素层次关系2 2 案例的各角色间交互图一2 4 案例的w e b 服务编排流程2 5 b p e l 描述的b u y e r ，s e l l e r ，s h i p p e r 抽象业务流程一2 7 p a t 检测结果截图3 2 p a t 给出的反例( 左图为w e b 服务编排，右图为w e b 服务编制) 3 2 服务结构图3 4 遗传算法运算过程4 0 服务组合样图4 5 抽象服务个数增长时算法收敛时间对比- 2 0 个抽象服务4 6 抽象服务个数增长时算法平均收敛时间对比4 8 服务实例个数增长时，5 0 次随机q o s 下激荡次数变化4 8 i l l l 2 1 2 3 4 5 6 7 8 1 1 2 3 4 5 1 l 2 2 2 2 2 2 2 2 3 4 4 4 4 4 图图图图图图图图图图图图图图图图 浙江大学硕士学位论文 表目录 表目录 表2 1w s c d l 和c s p 间的映射2 0 表2 2w s b p e l 和c s p 间的映射2 2 表3 1 各流程结构下的合成服务q o s 计算3 5 i v 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的 研究成果。据我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其 他人已经发表或撰写过的研究成果，也不包含为获得逝江盘堂或其他教育机 构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献 均已在论文中作了明确的说明并表示谢意。 学位论文作者签名： 签字日期：年月日 学位论文版权使用授权书 本学位论文作者完全了解逝姿盘堂有关保留、使用学位论文的规定， 有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅和 借阅。本人授权迸姿盘茔可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：导师签名： 签字日期： 年月日签字日期： 年月 日 浙江大学硕：l 学位论文第1 章绪论 1 1 研究背景 第1 章绪论 1 1 1s o a 与w e b 服务 随着i n t e r n e t 的深入发展，s o a 作为新一代的软件构架，将给软件产业带来 革命性的变化。在s o a 时代，任何一个大的应用软件系统，都不再由一个软件开 发商独立完成，而是由不同厂商生产的基于基础标准和接口的中间件相互协作完 成。随着s o a 的标准化，每种中间件的生产厂商的数量会逐渐减少，每个厂商也 只会专注于一种或几种中间件，努力提高中间件性能和质量。从软件产业总体上 看，这将降低软件开发成本，提高软件质量，大大减少目前各软件厂商之间相同 软件部分重复开发的问题。w e b 服务被认为是目前实现s o a 理念的最佳技术。w e b 服务技术吸收了分布式计算，网格计算和x m l 等各种技术的优点，通过采用 s o a p ，w s d l ，u d d i 等基于x m l 的标准和协议，解决了异构分布式计算以及代码和数 据重用问题，具有高度的互操作性，跨平台性和松藕合的特点，引起了世界范围 内工业界和学术界的广泛关注。目前在中国金融、电信、政府、电力、医疗卫生、 物流、电子商务、军队等行业的信息化建设中得到广泛应用。 面向服务架构( s e r v i c eo r i e n t e da r c h i t e c t u r e ，s o a ) 已成为当今i t 行业 的焦点，作为一种核心的架构理念，目前尚无对其的统一定义。 文献 1 对s o a 做出的定义如下：当代s o a 代表一个开放的、可扩展的、联 邦的、可组合的架构，促进面向服务并由自治的、高服务质量的、厂商多样的、 互操作的、可发现的和潜在可复用的服务组成，利用w e b 服务来实现。 w 3 c 在2 0 0 3 年公布的w e bs e r v i c ea r c h i t e c t u r e 草案呛3 中将w e b 服务定义 为：为支持机器之间跨越网络互操作而设计的软件，它使机器可处理形式描述接 口( 例如w s d l ) ，其它系统使用s o a p 消息与之通过服务描述所说明的方式进行交 互，典型地使用h t t p ，x m l 序列化以及其它w e b 标准传输s o a p 消息。w e b 体系结 构如图1 1 所示。 浙江大学硕士学位论文第1 章绪论 图1 1w e b 服务体系结构 可以看出，w e b 服务体系结构中共有三种角色： 1 ) 服务提供者( s e r v i c ep r o v i d e r ) ，可以发布自己的服务，并且对使用自身服 务的请求进行响应。 2 ) 服务注册中，i 二, ( s e r v i c er e g i s t r y ) ，也常被称为服务代理，用于注册已经发 布的服务提供者，对其进行分类，并提供搜索资源服务； 3 ) 服务请求者( s e r v i c er e q u e s t e r ) ，利用服务注册中心查找所需的服务，然 后使用该服务。 关于w e b 服务的相关协议正在标准化过程中，但目前业界已经形成了一套事 实上的协议栈，涉及w e b 服务互操作、组合与管理相关的一系列技术。w e b 服务 规范协议栈如图1 2 所示。 6 浙江大学硕士学位论文第1 章绪论 w c b 服务 殳计w s c d l w e b 服务编织一w s b p e i 。 书务 w e b j i l 务l 可靠w e b j l 强务安全 协作 性性 j 二f 文 u d d l w s d l s o a p x m l 。 t t 下p 1 l ( ) p j m s ，s m lp w e b n l l 务流程 w c b 服务质途 w c b 服务发脱 w c b n 疆务摊途 游怠 传输 图1 2w e b 服务规范协议栈 1 1 2w e b 服务组合的定义 随着i n t e r n e t 上w e b 服务的不断丰富，越来越多的w e b 服务被发布在网络 上，然而，这些服务大多功能单一、结构简单，无法满足企业复杂应用的需求。 如何有效组合分布于网络中的各种功能服务，实现服务的无缝集成，根据s o a 理 念的要求，将多个物理位置分散的w e b 服务在网络上组合成为功能更强大的组合 w e b 服务( c o m p o s i t ew e bs e r v i c e ) ，已经成为w e b 服务发展过程中的一个重要 步骤，也是关系到s o a 能否成功得到应用和实施的关键所在。通过服务组合，资 源得到了有效的重用，并能够更快捷、低成本地实现复杂功能，这将带来极大的 经济和社会效益。 w e b 服务组合正式在这种应用背景下被提出来的，w e b 服务组合是指基于面 向服务的体系结构，根据特定的业务目标，将多个已经存在的服务按照其功能、 语义以及它们之间的逻辑关系组装提供聚合功能的新服务的过程，是s o a 中实现 资源聚合与应用集成的主要模式口1 。 7 浙江大学硕士学位论文第1 章绪论 w e b 服务组合具有如下特点h 1 ： 1 ) 层次性和扩展性。w e b 服务的组合通过重用并组装已有的w e b 服务来生 成一个更大粒度的服务，使得组合的服务具有层次性和扩展性。 2 ) 动态与自适应性。w e b 服务组合是一个动态、自适应的过程，它在标准 协议的基础上，根据客户需求，对封装特定功能的现有服务进行动态地 发现、组装和管理。 3 ) 提高了组合与交易过程的自动化程度。w e b 服务组合通过动态的语义分 析进行服务的自动化匹配，减少了不必要的人工干预，易于实现动态电 子商务交易过程的自动化。 4 ) 提高软件生产率。通过重用已有的服务，并自动化地生成新的服务或系 统，极大地提高了软件的生产效率。 1 1 3w e b 服务组合方法 根据w e b 服务组合所依赖的技术基础，可以将其归纳为语义驱动的组合方法、 基于业务流程的组合方法、基于组件协作的组合方法和基于智能规划的组合方 法。 1 ) 语义驱动的服务组合方法 语义驱动的组合方法强调w e b 服务的自描述，其基本思想是建立w e b 服 务请求和描述的语义，推过推理自动生成合成服务。 常见的服务描述语言有：o w l s ，w s d l 以及其它自定义语言，对w e b 服务设定 了语义后，语义驱动的w e b 服务组合通过对服务组合图的搜索，生成组合方 案。在服务组合图上，最优组合方案表现为从起点到终点相邻语义关联程度 总和最大的一条路径。 当前w e b 服务缺乏足够的语义信息，需引入本体论和语义学知识，目前 尚处于研究初期，还需更深入地对本体进行研究，以获得一个更好的支持服 务组合的通用框架模型。由于语义w e b 服务开发负担较重，不能分布查询， 描述粒度尚局限在服务级别，所语义驱动的组合方法目前尚存不足瞄1 。 8 浙江大学硕七学位论文第1 章绪论 2 ) 基于业务流程的组合方法 基于业务流程的组合方法借鉴经典工作流1 的建模方法，认为组合服务 是构建在一组组件服务的基础上的业务流程，运用经典工作流的元素来描述 组合服务。组合服务建模的基本元素是活动、控制流和数据流。活动对应于 由组件服务执行的某个操作；控制流描述活动之间的依赖时序关系；数据流 描述组件服务之间的数据交换关系。基于业务流程的组合方法模型直观、易 于理解，且在运行环境的构造方面具有优势，但建模理论基础比较薄弱，因 此组合正确性难以保证。 基于业务流程的服务组合方法的特点在于：建模时依赖于开发者对于问 题本身的理解，自动化程度不高；模型与运行系统的映射简单，实现成本低。 3 ) 基于智能规划的服务组合方法 基于智能规划的服务组合方法将服务的自动组合问题抽象为一个规划 问题的自动求解，即给定一个初始状态和目标状态，在一个服务集合中寻求 一条服务的路径从初始状态到达目标状态的演变n 1 。可以看出，基于智能规 划的组合方法侧重于组合模型建立过程的自动化。目前这方面的工作主要是 借鉴智能规划领域的经典研究方法，如情景演算、规划域定义语言、定理证 明等，并与语义w e b 技术相结合，研究语义w e b 服务、组合目标分解、组合 推理以及组合服务模型的自动构造方法。基于智能规划的服务组合方法是一 个十分复杂的过程，目前这一方面理论尚处于探索阶段。 4 ) 基于组件协作的服务组合方法 基于组件协作的服务组合方法通过描述组件服务之间的消息编排来建 模组合服务，认为通过描述组合服务中各个参与方之间遵循的消息交换规范 就可以定义它们的协作行为，在组合中每个参与者引用组合描述并声明自己 的角色。例如，e b x m l 1 中的b p s s 提供了描述多参与方的组合中各方之间通 过消息交换实现的协作过程的基本框架。该组合方法着眼于消息交换行为， 对于描述多方参与的协作过程是一种较为直观的建模组合服务的方法。同 时，该方法与c s s ，p i 演算等描述并发进程间通信的形式化手段能够建立直 9 浙江大学硕士学位论文第1 章绪论 观的映射，支持组合模型行为性质的分析。 上述w e b 服务组合的四种技术方法各有优缺点，但均存在尚待发展完善的地 方，主要体现在以下两个方面： 1 ) 缺乏对w e b 服务组合的形式化验证技术，特别是非手工的工具化验证方 法 参加w e b 服务组合的各个组件服务运行在分布式异构环境下，因此组合 服务能否正确执行并成功满足用户需求是检验w e b 服务组合方法正确性和可 用性的标准。而试图依靠组合的w e b 服务的实际运行来检测组合中的错误是 代价昂贵且不实际的。所以在组合服务运行前进行形式化验证以保证服务组 合的正确性是非常重要的，而考虑到组件服务的数量庞大和可能的复杂内部 流程，一种非手工的工具化形式化验证方法尤其具有重要意义。 目前国内外制定了一系列基于工作流的w e b 服务组合规范，如w e b 服务编排 接口语言曲1 ( w e bs e r v i c e sc h o r e o g r a p h yi n t e r f a c e ，w s c i ) ，w e b 服务流语 言n 们( w e bs e r v i c e s f l o wl a n g u a g e ，w s f l ) ，w e b 服务商业流程执行语言 1 ( 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 e ，b p e l ) ，w e b 服务编排语言1 ( w e b s e r v i c e sc 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 ) 和商业流程建模 语言n 3 3 ( b u s i n e s sp r o c e s sm o d e li n gl a n g u a g e ，b p m l ) 。基于工作流的w e b 服 务组合规范可以分为两类：基于编排( c h o r e o g r a p h y ) 和基于编制 ( o r c h e s t r a t i o n ) 。基于编排的组合方法从一个全局的角度定义每个参与者 之间的会话和协作，是面向全局的；基于编制的方法则是局部的，从一个参 与者的角度定义了该参与者如何与其他w e b 服务进行交互。当前，b p e l 和 w s c d l 分别成为基于编排和编制的最为重要的w e b 服务组合规范。所以研究 w e b 服务组合的形式化验证技术主要是研究基于b p e l 和w s c d l 的形式化验 证方法。 2 ) 缺乏面向全局服务质量( o o s ) 目标优化的大规模服务选择算法 随着w e b 服务技术的推广，特别是在电子商务等领域的应用，服务的 q o s 成为面向服务计算系统的关键需求之一，所以o o s 感知的服务选择存在 1 0 浙江大学硕士学位论文第l 章绪论 现实的商业需求( 如s l a 管理) 。当前关于q o s 感知的服务选择问题的研究多 集中于小规模的q o s 局部优化的服务选择算法，但局部选择策略无法保证整 个组合服务的q o s 满足用户对合成后的组合服务的o o s 要求，面向全局q o s 优化的方法更能符合实际需求。另一方面，大规模的服务选择问题是未来面 临的问题，当服务组合的规模扩大后会呈现出新的特性，因此开展大规模w e b 服务选择的算法研究十分必要。综上面向全局q o s 目标优化的大规模服务选 择算法的研究具有重要意义。 1 2 当前研究现状 针对w e b 服务组合的形式化验证技术和面向o o s 优化的服务选择算法，下面 概述当前国内外在上述两个方向的研究方法和研究现状。 1 2 1w e b 服务组合验证方法 w e b 服务组合验证方法当前较成熟的主要有基于p e t r i 网、自动机理论和进 程代数三种形式化验证方法。 1 2 1 1 基于p e t r i 网的服务组合验证 p e t r i 网具有直观的图形表示方法和丰富的形式化语义，且存在很多系统分 析验证手段，所以被作为一种形式化工具而广泛应用于流程分析和验证n4 1 。文献 1 - 1 5 利用p e t r i 网对服务建模，将服务的操作和输入输出分别映射为p e t r i 网 中的转移( t r a n s i t i o n ) 和库所( p l a c e ) ，并对服务组合中的各种基本结构( 如顺 序、互斥、并发等) 和高级结构( 如并发、同步等) 映射到p e t r i 网。在服务组 合模型和p e t r i 网模型问建立了一一对应后，服务组合的验证问题就转化为p e t r i 网的活性、有界性、和死锁活锁等特性的检验，而这些特性的检验可以应用已 成熟的p e t r i 网验证工具和理论。文献 1 6 将描述工作流执行流程的任务构造算 子映射为p e t r i 网，利用p e t r i 网来刻画任务构造算子的语义，然后已有的基于 p e t r i 网的分析验证方法可用于检查和验证。文献 1 7 在此基础上开发了基于 p e t r i 网的工作流验证工具w o f l a n 。文献 1 8 以服务描述语言d a m l s 为基础， 浙江大学硕士学位论文第l 章绪论 将d a m l - s 中的服务流程模型通过工具自动转化为p e t r i 网，然后利用p e t r i 网 对服务组合流程进行自动的分析检测。文献 1 9 为了验证b p e l 的全局抽象流程 和各参与者的局部可执行流程之间的一致性，利用p e t r i 网对b p e l 进行建模， 并利用工具w o m b a t 4 w s 进行自动验证。文献 2 0 ，2 1 基于p e t r i 网或有色p e t r i 网进行w e b 服务组合。 1 2 1 2 基于自动机理论的服务组合验证 文献 2 2 2 4 利用有限状态自动机来形式化描述w e b 服务的动态行为。该模 型用一个抽象的概念一行为来描述w e b 服务能提供的操作，用状态的迁移来描述 w e b 服务行为的逻辑顺序。在用有限状态自动机来形式化描述w e b 服务的基础上， 定义了一个w e b 服务组合的通用框架，在该框架中，利用动态命题逻辑 ( p r o p o s i t i o n a ld y n a m i cl o g i c ，p d l ) 对一组已有的w e b 服务的形式化模型进行 推理计算，从而得出满足用户要求的w e b 服务组合方案。文献 2 5 - 2 7 从服务之 间的消息交互出发，将服务形式化描述为一个具备先进先出输入消息队列的非确 定b u c h i 自动机，将服务组合视为服务之间通过异步消息传递的全局会话协议 ( c o n v e r s a t i o np r o t o c 0 1 ) ，提出了会话协议的可行性条件和异步消息的可同步 化条件。可行性指存在符合会话协议的服务组合；可同步化指服务异步消息模式 可等价转换为同步消息模式。然后将这些条件和目标属性用线性时序逻辑描述为 断言，最后模型检测工具s p i n 可用于进行模型检测，从而判断服务组合是否符 合预定的会话协议。文献 2 8 采用有限状态自动机对基于b p e l 描述的服务组合 流程进行建模，然后应用模型检测工具检查流程安全性和活性。 1 2 1 3 基于进程代数的服务组合验证 进程代数是用来对动态软件实体进行建模的形式化语言，具有严密定义的形 式化语义，能够将服务的动态行为与清晰的操作语义联系起来。它包括了通信系 统演算( c a l c u l u so fc o m m u n i c a t i n gs y s t e m s ，c c s ) 啪，通信顺序进程 ( c o m m u n i c a t i o ns e q u e n c ep r o c e s s ，c s p ) 咖1 和p i 演算b 等。文献 3 2 指出了应 1 2 浙江大学硕士学位论文 第1 章绪论 用进程代数形式化描述w e b 服务和w e b 服务组合对于服务组合验证的意义，并示 例了如何用进程代数表达w e b 服务编排和编制。文献 3 3 用c c s 对w e b 服务编排 协议w s c i 进行形式化建模，并对参与交互的服务进行兼容性和可替换性分析， 并对无法正常交互的服务，提供了适配器机制以实现二者的通信。关于b p e l 的 模型验证研究成果较多，文献 3 4 提出了进程代数( p r o c e s sa l g e b r a ) 和b p e l 间 映射的框架。文献 3 5 把b p e l 映射为p r o m e l a 语言，然后用工具s p i n 进行形式 化验证。w s - c d l 也有不少验证方法被提出，g d i a z 等人用时态自动机模型化 w s - c d l ，将时态自动机作为中间模型来检测w e b 服务编排的正确性d 6 1 。文献 3 7 建立了服务编排的本体框架。文献 3 8 定义了简单的形式化语言c l 描述w s - c d l ， 但w s c d l 的重要组成部分w o r k u n i t 没有包含。文献 3 9 提出了w s c d l 的形式 化模型框架a b s t r a c tw s c d l 和a b s t r a c tw s c d l 与p i - 演算间的映射规则，最 后基于p i 一演算的工具进行形式化验证。文献 4 0 用f s p ( f i n i t es t a t ep r o c e s s ) 形式化验证w s - b p e l 和w s c d l 的一致性。 上述三种对服务组合进行形式化验证的方法尽管在形式化模式，数学理论方 面各不相同，但针对w e b 服务组合的验证能力基本相同。同时在运用的方便性和 复杂程度上有较大差异。p e t r i 网和自动机理论对服务组合的描述较为直观，但 当服务规模变大，服务数量增多，服务间交互情况复杂的情况下，会引起状态空 间的爆炸，所以，p e t r i 网和自动机理论的形式化验证方法会随着服务组合规模 和复杂度的增长而引起验证代价的急剧增大。而基于c s p 进程代数的形式化验证 方法由于采用了文本的进程表达式描述系统，其表达形式简洁，且对服务规模和 服务之间复杂度敏感度较小。所以本文采用基于c s p 进程代数的形式化方法进程 服务组合的验证。 基于编排的w e b 服务组合规范w s c d l 和基于编制的w e b 服务组合规范 w s b p e l 并不是孤立的，二者位于不同层次上而被结合起来用于实现w e b 服务组 合：首先根据业务需求，w s - c d l 从全局的角度描述参与组合的各个子服务之间的 相互协作过程，然后将全局的协作过程映射到每个局部角色，得到每个局部角色 的行为，即w s b p e l 描述。目前基于进程代数的形式化验证方法有较多研究集中 浙江大学硕士学位论文第l 章绪论 于w s - c d l 和w s - b p e l 各自独立的形式化验证，但w s - c d l 和w s - b p e l 间的一致性 验证甚少涉及，而该问题的解决对于w e b 服务组合验证是个重要问题，也是本文 着力研究的第一个问题。 1 2 2q o s 感知的w e b 服务选择算法 主流的e o s 感知的w e b 服务选择算法可以分为两类：传统的规划算法和基于 智能优化算法。 1 2 2 1 基于传统规划算法的w e b 服务选择 文献 4 1 将w e b 服务选择问题映射为o 一1 背包问题( o 一1m u l t i d e m e n s i o n k n a p s a c kp r o b l e m ，m m k p ) ，每个抽象服务的候选服务集对应于0 1 背包问题中 的一个物品包，n 个抽象服务的组合服务流程对应n 个物品包，而抽象服务的每 个候选服务相当于每个物品包中的物品，候选服务的q o s 约束属性对应于物品的 费用属性，q o s 优化目标属性对应于物品的价值。因此，w e b 服务选择问题转化 为多个物品包的0 1 背包问题。然后，成熟的解决0 - i 背包问题的算法如分支定 界法( b r a n c h - a n d b o u n dm e t h o d ) 等可运用进行包的选择。文献 4 1 还提出运用 图的方法，把w e b 服务选择映射为有向无环图( d i r e c t e da c y c l i cg r a p h ，d a g ) 后，变为一个多约束的优化路径选择问题。文献 4 2 提出一个映射框架建立服务 覆盖网络( s e r v i c eo v e r l a yn e t w o r k ，s o n ) ，然后转化服务选择问题为图的路径 选择问题，最后用d ij k s t r a 的最短路径选择算法得出优化的选择结果。 1 2 2 2 基于智能优化算法的w e b 服务选择 智能优化算法是一类通过模拟某一自然现象或过程而建立起来的优化方法， 这类算法包括遗传算法、禁忌搜索、粒子群算法、模拟退火等。遗传算法作为一 种智能优化方法，具有并行计算、群体寻优的特点，同时不同于加权法等传统的 目标寻优方法，遗传算法( g e n e t i ca l g o r i t h m ，g a ) 不需要与应用背景相关的启 发式知识只需要目标函数和相应适应值函数。文献 4 3 4 5 将简单遗传算法 ( s i m p l eg e n e t i ca l g o r i t h m ，s g a ) 用于基于q o s 属性计算的w e b 服务选择过 1 4 浙江大学硕士学位论文第1 章绪论 程中，简单遗传算法中的每条染色体相当于一个w e b 服务组合的方案，而染色体 的每个基因位对应于服务流程中一个抽象服务，在遗传算法的交叉变异操作中， 基因位的取值为抽象服务所包含的候选服务集。通过遗传算法种群的不断进化， 优化目标也不断得到提高。粒子群优化算法( p a r t i c l es w a r mo p t i m i z a t i o n ，p s o ) 是一种进化计算技术，源于对鸟类捕食的行为研究。文献 4 6 将粒子群优化算法 应用于w e b 服务选择，其基本思想是：首先产生一定数目的粒子群，每个服务组 合流程编码为一个粒子，每一个粒子利用本身信息、局部较优信息和全局较优信 息3 个信息，产生具有更高目标值的新粒子。这一过程不断进行，实现在解空间 的并行全局搜索；算法停止时，得到一组粒子集合，对应于多条收敛于p a r e t o 优化或近似优化路径的组合集。 其中文献 4 3 对比了遗传算法和传统规划算法在w e b 服务组合领域的应用， 得出遗传算法具有如下优点：一方面，对约束和目标函数是否为线性没有要求， 这是源自遗传算法对问题域的独立性；另一方面，w e b 服务组合规模增长时遗传 算法的时问性能优于传统规划算法。 对于组合规模较大的q o s 全局优化的w e b 服务组合问题，遗传算法更适合 应用于本领域。s g a 用于w e b 服务选择过程4 3 4 5 1 显现出较好的时间性能，但目 前这些研究主要集中于1 0 5 1 0 2 0 个执行计划的中小规模w e b 服务组合问题，针对 大规模服务组合的研究还很少。所以研究基于改进遗传算法的针对服务组合规模 较大的服务选择算法是本文研究的第二个问题。 1 3 研究内容 w e b 服务组合是热门研究问题，本文着重展开服务组合验证和w e b 服务选择 算法的相关问题研究。研究成果体现在如下两个方面： 1 ) 基于c s p 的w e b 服务编排和编制一致性检查。在设定的转化规则一f ，w e b 服务编排语言w s - c d l 和w e b 服务编制语言w s - b p e l 被映射为c s p 语言， 然后基于c s p 的模型检测工具p a t 将进行二者的一致性检测。并给出了 检测案例。 浙江大学硕士学位论文第l 章绪论 2 ) 提出大规模w e b 服务选择算法g a e l s 。针对候选服务众多的大规模w e b 服务选择问题，提出一种新的w e b 服务选择算法g a e l s ( g e n e t i c a l g o r it h me m b e d d e dl o c a ls e a r c h i n g ) ，该算法运用高适应度初始种群 和局部搜索的变异策略，加快收敛速度。通过实验评测表明与简单遗传 算法相比，g a e l s 算法能更快得到近似最优解，且随着服务规模增长， 拥有更好的适应性。 1 4 论文结构 本论文的结构是：第2 章详细描述了服务编排和编制一致性检查的理论，在 介绍c s p 语言和模型检测理论的基础上，给出服务编排和编制一致性检查的各个 步骤，并给出了一个案例；第3 章是o o s 全局优化的w e b 服务选择模型，基于用 户偏好和多维q o s 模型，w e b 服务选择问题的数学模型是单目标多约束的最优化 问题；第4 章详细阐述了大规模w e b 服务选择的算法g a e l s ，并给出了实验评测； 最后第5 章总结了本论文的工作和今后研究展望。 1 6 浙江大学硕士学位论文第2 章w e b 服务编排和编制一致性检查 第2 章w e b 服务编排和编制一致性检查 w s - b p e l 和w s - c d l 分别成为基于编排和编制的最为重要的w e b 服务组合规 范。二者位于不同层次上而被结合起来用于实现w e b 服务组合：首先根据业务需 求，w s - c d l 从全局的角度描述参与组合的各个子服务之间的相互协作过程，然后 将全局的协作过程映射到每个局部角色，得到每个局部角色的行为，即w s - b p e l 描述。服务编排和编制的描述一致性需要得到保证。本章提出基于c s p 的服务编 排和编制一致性检查方法。 本章2 1 节介绍了c s p 语言，然后2 2 节概述了模型检测理论和模型检测工 具p a t ；在2 3 节详述了基于c s p 的服务编排和编制一致性检测方法，最后在2 4 节给出了一个详细案例。 2 1c s p 语言 通信顺序进程( c o m m u n i c a t i o ns e q u e n c ep r o c e s s e s ，c s p ) 是h o a r e 于1 9 7 8 年建立的一种适合于分布式并发软件规格和设计的形式化方法h 7 1 。c s p 主要包括 进程和事件，一个c s p 进程与其他进程或观测者交互的唯一途径就是通信。通信 表现为可见事件和动作形式，进程还可以执行代表内部进展的不可见动作。c s p 语言的巴科斯范式如下： p 曼= s t o pa pi a ：a 专只ij p 【】j p p h p i p pp l s k i pl p ；p j p i | 尸ij p a a 假设口为事件，p 为进程，那么s t o p 表示死锁进程；口一p 表示事件引发进 程；口：a 一尸口表示事件集合彳中任一事件口发生，引发进程集合尸。中相应进程； 给定两个进程尸和q ，尸【】q 的行为依据进程p 和q 的第一个执行事件来决定将执 行的进程，也称外部选择；而p f i q 称为内部选择，行为为进程p 或进程q 的行为， 是一种非确定的行为；p q 的行为是当进程p 执行了一段时间后将转向进程 q ：s k i p 的行为是什么也不做然后成功终止；p ；q 的行为时进程p 执行完后进入进 1