（计算机应用技术专业论文）基于pi演算的服务流验证方法研究.pdf

浙江大学硕士学位论文摘要 摘要 为了满足企业应用系统业务的快速变化，一种新的软件系统架构理论面向 服务的架构s o a ( s e r v i c e - o r i e n t e da r c h i t e c t u r e ) 应运而生，并引领着软件行业 新一轮的技术变革。s o a 是以服务为基本单位，通过服务重用和快速组合构建 随需应变的松耦合分布式系统，由于单个的w e b 服务能够提供的功能有限，为 了更加充分地利用共享的w e b 服务构建企业级应用系统，w e b 服务组合技术变 得愈加重要。 w e b 服务组合验证是在服务组合实际部署前，提前发现w e b 服务组合中存 在的问题的技术，是w e b 服务组合走向实用的前提和关键。论文结合实验室承 担的国家支撑计划、8 6 3 计划等国家级重大科研攻关项目，针对验证服务组合内 部服务流程逻辑的正确性问题展开研究，探索基于p i 演算的服务流验证方法， 论文主要内容如下： 1 基于p i 演算的s f d l 模型转换技术。p i 演算作为一种表达能力强大、形式 简洁的形式化方法，特别适合用来描述分布式松耦合的并发系统。论文首先 研究如何用p i 演算建模常见的流程结构模式。然后在分析服务组合描述语 言b p e l ( 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 ) 和工作流描述语言x p d l ( x m lp r o c e s sd e f i n i t i o nl a n g u a g e ) 的基础上，提出了服务流程描述语言 s f d l ( s e r v i c ef l o wd e f i n i t i o nl a n g u a g e ) ，该语言基于x m l ，易于理解，表 达能力强。为实现基于p i 演算的服务流验证，论文采用基于模式的算法， 实现了从s f d l 到p i 演算表达式的整体模型转换。 2 基于p i 演算的服务流验证方法。论文通过p i 演算的操作语义、自动推演等 理论来识别和验证服务流验证中存在状态的可到达性、流程的可完成性等问 题。存在上述问题的服务流在转换成p i 演算表达式后都无法顺利推演成空 进程。本章还分析了利用m w b 等工具进行自动化验证的优缺点，针对难以 与现有系统集成等问题，论文提出对应的解决方案：在系统中进行p i 演算 推演，在推演过程中依次检查服务流的状态可达性、死锁等问题。 3 基于p i 演算的服务流验证原型系统实现。为了验证论文所提方法，基于课 题组已有的w e b 服务组合框架w s c f 和w e b 服务组合原型系统 j t 觚g f l o w s ，论文实现了所提出的基于p i 演算的s f d l 模型转换和服务流 验证方法，系统和实验表明论文所提的算法有较高的准确率。 关键字：面向服务的体系架构( s o a ) ，w e b 服务，服务组合，p i 演算，服务组 合验证 浙江大学硕士学位论文 a b s t r a c t a bs t r a c t t om e e tt h e r a p i dc h a n g e o fe n t e r p r i s eb u s i n e s sr e q u i r e m e n t s ，s o a ( s e r v i c e o r i e n t e da r c h i t e c t u r e ) ，an e ws o f t w a r ea r c h i t e c t u r e , i sp r e s e n t e d , a n dl e a d sa t e c h n o l o g i c a lr e v o l u t i o no fs o f t w a r ei n d u s t r y w e bs e r v i c ei st h eb a s i cc o m p o n e n to f s q 九w h i c hi su s e dt oc o n s t r u c t d i s t r i b u t e d , l o o s e - c o u p l e de n t e r p r i s e - s c a l e a p p l i c a t i o ns y s t e m so nd e m a n d as i n g l ew e bs o l v i c ec a no n l yp r o v i d el i m i t e d f u n c t i o n s i no r d e rt os h a r ew 曲s e r v i c e so nt h ei n t c r n e t , i ti sv e r ye s s e n t i a lt o c o m b i n et h ee x i s t i n gs r v i 懈i n t oc o m p o s i t es e r v i c eo ri n f o r m a t i o ns y s t e m v e r i f i c a t i o no fw e bs e r v i c e sc o m p o s i t i o ni st of i n d t h e p r o b l e m so ft h e c o m p o s i t i o nb e f o r ed e p l o y m e n t , w h i c hi st h ek e yf o rw e bs a r v i c e sc o m p o s i t i o n b c c o m c sp r a c t i c a l t h i st h e s i s ，w h i c hi sb a s e do nn a t i o n a ls u p p o r tp l a na n d8 6 3 r e s e a r c hp r o j e c t so fo u rl a b ，e m p h a s i z e st h ef o r m a lv e r i f i c a t i o no fw e bs e r v i c e sf l o w t h em a j o rw o r kh a st h r e ep a r t s ： 1 p i - e a l e u l u s b a s e dm o d e l i n go fs f d l p i c a l c u l u si sap o w e r f u la n db r i e ff o r m a l m e t h o d , w h i c hi sf i tt om o d e lt h el o o s e - c o u p l e d c o n o t t r r e n ta n dd i s t r i b u t e d s y s t e m s f i r s t l y , g e n e r a lf l o wp a t t e r n sa r em o d e l e db yp i c a l c u l u s t h e ni t i n t r o d u c e san e ws e r v i c e s c o m p o s i t i o nl a n g u a g e ： s f d l ( s e r v i c ef l o w d e f i n i t i o nl a n g u a g e ) w h i c hi sb a s e do nt h eb p e la n dx p d l s f d l , w h i c hi s b a s e d0 1 1 此，i se a s yt ou n d e r s t a n d a c c o r d i n gt ot h ec h a r a c t e r i s t i c so fs f d l w e p r e s e n ta l g o r i t h m sb a s e do i lm o d e sf o rp i c a l c u l u s - b a s e dm o d e l i n go fs f d l 2 p i - c a l c u l u s b a s e dv e r i f l c a t i 仙o fw e bs e r v i c e sf l o w t h er e s e a r c hs c o p eo f v e r i f i c a t i o no fw e bs e r v i c e sf l o wi n c l u d e sr e a c h a b l eo fa c r i d t i e s d e a d l o c k ，l i v e l o c ka n ds oo i lt l l i st h e s i sv e r i f i e st h ep r o b l e m so fw 曲s e r v i c e sf l o ww i t ht h e o p e r a t i o n a ls e m a n t i c s a u t o m a t i cd e d u c t i v eo fp i c a l c u l u s t h ep r o c e s s e sw i t l l p r o b l e m sw i l ln o tb ed e d u c t i v et oan u l lp r o c e s s i ti n t r o d u c e sh o wt ou s e m w bt oa u t o m a t e dv e r i f i c a t i o na n di t sa d v a n t a g e sa n dd i s a d v a n t a g e s t o i n t e g r a t e 诵t he x i s t i n gs y s t e m sa n ds o l v eo t h e rp r o b l e m s m e t h o d sa n da l g o r i t h r n s a l ep r e s e n t e dt oi m p r o v ea u t o m a t e dv e r i f i c a t i o n t h es o l u t i o ni sd e d u c i n gt h e p r o c e s s e so fp i - c a l c u l u si no u rs y s t e m sa n dv e r i 研n gt h e s ep r o c e s s e ss t a t e s d u r i n gd e d u c t i o n 3 p r o t o t y p eo fp i - c a l c u l u s b a s e dv e r i f i c a t i o no fw e bs e r v i c e sf l o w ri n t r o d u c e s w s c f ( w e bs e r v i c ec o m p o s i t i o nf r a m e w o r k ) a n di t sp r o t o t y p e - j t a n g f l o w s a n d j t a n g f l o w - si m p l e m e n t st h ea l g o r i t h m sa b o u tp i - c a l c u l u s - b a s e dv e r i f i c a t i o n o f w e bs e r v i c e sf l o w e x p e r i m e n t ss h o wt h e s ea l g o r i t h m sa r ep r a c t i c a l k e y w o r d s ：s e r v i c e - o r i e n t e da r c h i t e c t u r e ( s o a ) ，w e bs e r v i c e ，w e bs e r v i c ec o m p o s i t i o n , f i - c a l c u l u s ，f o r m a lv e r i f i c a t i o n 浙江大学硕士学位论文图目录 图目录 图1 1s o a 概念层次。2 图1 2w e b 服务的基本模型3 图1 3w e b 服务规范3 图1 4 论文组织架构8 图2 iw e b 服务组合的研究内容 1 0 图2 2 状态不可达的三种情况l l 图2 3 节点e 被多次激活1 2 图2 4p e t r i 网图形表示13 图2 5w e b 服务的p e t r i 网建模1 3 图3 1s f d l 的s c h e m a 文件截图2 2 图3 2 顺序模式2 6 图3 3 并行分支厶2 6 图3 4 同步模式2 6 图3 5 唯一选择模式。2 7 图3 6 简单汇聚模式2 7 图3 7 多汇聚模式2 7 图3 8 鉴别器模式2 8 图3 9j t a n g f l o w d e s i g n e r 中复杂合并模式截图。2 8 图3 1 0 节点d 的入线模式截图2 9 图3 1 1 复杂合并模式2 9 图3 1 2j t a n g f l o w d e s i g n e r 中循环回迁模式截图2 9 图3 13 循环回迁模式3 0 图3 1 4 多实例模式3 0 图3 1 5 模型结构的化简前3 l 图3 1 6 模型结构的化简后3 l 图3 1 7 网上购物流程。3 2 图3 1 8 简化后的网上购物流程。3 3 图4 1 验证流程3 5 图4 2 死锁3 8 图4 3 典型的循环结构3 9 图4 4 回迁迁移a 被正确标识为循环类型4 0 图4 5 回迁迁移a 未被正确标识为循环类型如 图4 6 路由设置不平衡4l 图4 7 带有活锁的流程：4 3 图4 8 进程描述文件l o o p a g 4 3 图4 9 导入进程4 3 图4 1 0 用s t e p 命令进行p i 演算的推演4 4 图4 1 l 验证流程图4 5 图4 1 2p i 演算推演4 8 图5 1w s c f 模块图5 2 v 浙江大学硕士学位论文图目录 图5 2 ，r a n g f l o w d e s i g n e r 模块图5 3 图5 3y r a n g f l o w d e s i g n e r 界面截图：5 4 图5 4 验证模块类图 图5 5 语法验证截图5 6 图5 6 带有错误的网上购物流程 图5 7 右键菜单“验证工程”5 7 图5 8 验证结果 v i 浙江大学硕士学位论文 表目录 表目录 表2 1w e b 服务和p i 演算元素对应表1 5 表3 1 工作流和服务组合的比较。2 l 表3 2s f d l 活动类型及其功能2 3 表3 3 入线和出线模式2 3 表3 4 工作流模式列表2 5 续表3 5 工作流模式列表2 6 表3 6 化简后s f d l 节点和p i 演算进程对应表3 3 表5 1j t a n g f l o w d e s i g n c r 模块功能说明5 3 表5 2 验证错误信息及其解决方案5 8 v n 浙江大学研究生学位论文独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的 研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得逝江盘鲎或其他教育机构的学位或 证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意。 靴论文作者签名：貔概签字嗍加莎年月6 同 学位论文版权使用授权书 本学位论文l 乍者完全了解逝望盘堂有权保留并向国家有关部门或机 构送交本论文的复印件和磁隘，允许论文被查阅和借阅。本人授权逝江盘茎 可以将学位论文的全部或部分内容编入有关数据库进行检索和传播，可以采用影 印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 导师签名： 签字同期：7 9 年莎月6 同 签字r 期：年月日 浙江大学硕士学位论文第1 章绪论 第1 章绪论 面向服务的体系架构( 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 】正引领着软件行 业的新一轮发展潮流，并在未来给软件和网络带来革命性的变化。重用已有的组 件或服务是s o a 的核心思想，而w e b 服务和w e b 服务组合技术作为s o a 实现 上述思想的关键技术，其技术标准不断成熟，应用不断增多。但w e b 服务组合 在投入实际应用前，可能存在问题，其正确性验证是必不可少的。w e b 服务组合 验证能在服务部署前提前发现问题，大大提高w e b 服务组合应用系统的稳定性 和健壮性。w e b 服务组合验证技术已经成为s o a 系统从概念走向实际应用的关 键。 1 1 研究背景 当今的企业和公共事业机构，其业务面临着步入知识经济时代、全球化、扁 平化的快速巨变。s o a 具有松耦合、基于标准的开放性和集成能力强等特点， 能够很好地帮助企业软件系统面对这一挑战。 1 1 1s o a 的概念、内容与发展 目前还没有一个统一的s o a 定义，但一般认为s o a 是一种架构模型，一般 是指为了满足在网络环境下业务集成的需要，通过连接能完成特定任务、独立功 能的实体来实现业务逻辑的一种软件系统的架构，它是基于服务的企业n 基础 架构的思想、方法、风格、工具的一个总称【2 1 。 在传统方法中，我们总是先构建一个个的应用，每个应用可能有自己的功能 层次、数据架构、安全架构等，然后随着系统的发展，需要在应用间进行整合， 包括表示层整合、数据整合和流程整合等。s o a 却希望企业i t 系统不是完全以 应用为中心，而是以服务为中心对象构建。s o a 方法将功能方面涉及的对象、 数据、组件、业务流程、界面等从服务提供者和消费者角度进行层次化。与此同 时，将安全架构、数据架构、集成架构、服务质量管理等应用共用的功能提取出 来形成不同的层次，为所有服务共用。 文献 2 1 将s o a 架构分为了8 个层次，从底层到高层分别是：遗留系统、服 务组件层、服务层、业务过程合成、表示层、企业服务总线、基础架构层和数据 架构及商业智能层，如图1 1 所示： 浙江人学硕士学位论义 第1 章绪论 图1 1s o a 概念层次 s o a 可以根据需求通过网络对松散耦合的粗粒度应用组件进行分布式部 署、组合和使用。这种具有中立的接口定义( 没有强制绑定到特定的实现上) 的 特征称为服务之间的松耦合。松耦合系统的好处最大的好处是它的灵活性，当组 成系统的单个服务的内部结构和实现发生改变时，系统能够继续存在，其它的服 务并不需要做更改。 对松耦合的系统的需要来源于业务应用程序需要根据业务的需要变得更加 灵活，以适应不断变化的环境，比如经常改变的政策、业务级别、业务重点、合 作伙伴关系、行业地位以及其他与、l k 务有关的因素，这些因素甚至会影响业务的 性质。能够灵活地适应环境变化的业务一般被称为按需业务。在按需业务中，一 旦需要，就可以对完成或执行任务的方式进行必要的更改。 从2 0 0 4 年8 月，i b m 将s o a 概念引入中国。三年多来，随着互联网的快 速发展，在i b m 、b e a 、o r a c l e 、s a p 等国际巨头们的大力推动下，中国已经处 于s o a 试验和局部部署阶段，显然以服务为导向的s o a 部署将要成为中国企业 未来信息化建设的核心部件，中国正加速步入s o a 的成熟季节。 1 1 2w e b 服务技术框架 s o ar 卜1 的服务是构建在一系列基于开放标准的基础之上的功能构件。w e b 服务定义了如何在异构系统之间实现通信的标准化方法，使服务可以跨越运行平 台和实现语言。 浙江大学硕士学位论文 第1 章绪论 图1 2 w e b 服务的墨本模型 w e b 服务是一种部署在w e b 上的对象或组件，一个完整的w 曲服务架构包 括三种角色：w 曲服务提供者、w e b 服务请求者和w e b 服务中介。如图1 2 所 示，w e b 服务基本模型包含三类角色： 服务提供者( s e r v i c ep r o v i d e r ) ：可以发布自己的服务，并且对使用自身服 务的请求进行响应； 服务注册中心( s e r v i c er e g i s t r y ) ：用于注册已经发布的s e r v i c ep r o v i d e r ， 并对其进行分类，并提供搜索服务； 服务请求者( s e r v i c er e q u e s t o r ) ：利用服务注册中心查找所需的服务，然后 使用该服务。 w e b 服务框架中的上述三种角色之间使用了如下三种操作进行交互： 发布( p u b l i s h ) ：服务请求者向服务注册中心注册自己的功能和访问接口； 查找( f i n d ) ：服务请求者通过服务注册中心查找特定的服务； 绑定( b i n d ) ：服务请求者使用服务。 图1 3 w e b 服务规范 w e b 服务是自我包含的、模块化的应用系统，可以通过网络连接进行访问。 为了在互联网范围内实现大规模的分布份应用，必须使用一系列标准和协议来实 现不同编程语言或平台的互操作。如图1 3 所示，w 曲服务体系使用w s d l ( w e b s e r v i c e sd e s c r i p t i o nl a n g u a g e ) t 3 】来描述服务，使用u d d i ( u n i v e r s a ld e s c r i p t i o n ， 浙江大学硕士学位论文 第1 章绪论 d i s c o v e r ya n di n t e g r a t i o n ) 4 】来发布、查找服务，使用s o a p ( s i m p l eo b j e c ta c e s p r o t o c 0 1 ) 5 】来调用服务。 1 1 3w e b 服务组合及相关技术方案 随着w e b 服务技术的日益成熟，越来越多的稳定易用w e b 服务部署在网络 上供用户共享。但单个的w e b 服务能够提供的功能有限，为了更好地利用已有 的共享w e b 服务，有必要将这些w e b 服务组合起来，提供更为强大的服务功能、 加快构建应用系统，以便更好地满足用户需求。 w e b 服务组合【6 】是指当单个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 的工作流描述语言和工作流技术为基 础，具有代表性的有b p e l 和w s c d l 等【2 6 】【2 7 1 1 2 扪。工作流( w o r kf l o w ) 就是 工作流程的计算模型，即将工作流程中的工作如何前后组织在一起的逻辑和规则 在计算机中以恰当的模型进行表示并对其实施计算。工作流要解决的主要问题 是：为实现某个业务目标，在多个参与者之间，利用计算机，按某种预定规则自 动传递文档、信息或者任务。简单地说，工作流就是一系列相互衔接、自动进行 的业务活动或任务。我们可以将整个业务过程看作是一条河，其中流过的就是工 作流。静态w e b 服务组合和普通的工作流有很多相似的地方： 一需首先建立一个流程模型，然后在执行引擎中执行该流程； 流程中都有特定的数据流和控制流； 由执行引擎控制流程的路由方向，并调用相关的应用或服务等。 所以有些研究人员也称静态w e b 服务组合为服务流。 4 浙江大学硕士学位论文第1 章绪论 现有的w e b 服务组合描述语言主要有两类：人工智能的方法，如语义w e b ； 基于流程的方法，如b p e l 等。而根据w e b 服务组合的实现方式可以分为服务 编制和服务编排，前者以b p e l 为代表，后者以w s c d l 为代表。 虽然除b p e l 之外还有一些业务流程规范，但到目前为止，b p e l 是最为成 熟和被广泛支持的规范。b p e l 是基于x m l 语言开发的协议，支持面向流程的 服务组合。该协议由b e a 、i b m 、m i c r o s o i t 、s a p 和s i e b e l 等公司提出，融合 了早期的ibm 的w e bs e r v i c e sf l o wl a n g u a g e ( w s f l ) 和微软的x l a n g 规范的 很多特点。在b p e l 中组合的服务称作流程，组合中的服务、合作者和信息交 换等操作都叫做活动。b p e l 具有很高的灵活性，支持嵌套组装，并且有很强的 扩展性。一些与服务组装的业务逻辑无关的属性，如服务质量( q o s ，q u a l i t yo f s e r v i c e ) ，事务处理等可以被作为附加扩展，由具体实现平台进行处理。 w s c d l 用于精确描述任意类型的业务流程服务之间的对等协作，它从全局 的角度出发，定义不同网络服务参与者为实现某一共同商业目标在预定义的规则 下进行信息交换，妙法服务之间的协同作业。w s c d l 是非执行的抽象业务流程 规范，它不依赖于任一合作方内部的具体流程实现语言，不仅支持对任意数量的 服务之间的协作的描述，同时也支持对等协作中的异常处理和事务处理。 b p e l 和w s c d l 的共同点是都以一种面向流程的方式把多个w e b 服务组 织起来，完成一个复杂的新业务流程，实现单一基本w e b 服务无法实现的功能。 其区别在于服务编制一般需要一个工作流引擎来完成业务流程的执行，而服务编 排更多得依赖多个w e b 服务协作完成。本文的研究重点主要是基于服务编制生 成的基于流程的w e b 服务组合。 1 1 4w e b 服务组合验证 通过w e b 服务组合可实现复杂的新业务流程，但如何判断组合的w e b 服务 可实现预期的业务需求，如何判断组合的w e b 服务不会在运行中出现问题，这 成了企业真正应用w e b 服务组合前必须认真考虑的重要问题。 事实上，经过人工设计或自动构建完成的服务组合可能存在众多问题，可能 发生死锁、活锁、状态不可达等问题，如果不进行事先验证，等这些问题在实际 实施时暴露出来，必然会带来重大损失。因次，在服务流程执行以前，最重要的 工作就是对流程定义进行分析和验证。 当前国内外研究人员对w e b 服务组合验证并没有严格的定义，这里采用文 献【6 】的分类方法，将w e b 服务组合验证问题分为两大类： 1 验证服务组合内部服务流程逻辑的正确性； 2 验证服务组合中各服务间的兼容性。 本文的重点是前一部分。而服务组合内部服务流程逻辑的正确性验证和传统 5 浙江大学硕士学位论文第1 章绪论 工作流的验证有很多相似之处，所以这里借鉴工作流验证的定义给出w e b 服务 组合验证的定义： w e b 服务组合验证是服务组合投入实际使用前，使用一定的规则和定义对 服务组合中服务间的兼容性和服务组合内部流程逻辑进行的一种检查。 服务组合中的各服务间的兼容性验证其主要目标是检验服务组合中各服务 间能否正常协作。可将其细分为三个方面： - 服务间语法的兼容性，指服务问能否实现语法层面的正常交互； 服务间语义的兼容性，指服务间在服务功能、参数含义、消息内容等方 面保持语义的一致性： 服务间行为的兼容性，是验证交互的服务能否在不违反各自内部服务逻 辑的前提下，完成和其它服务的交互。 服务组合内部服务流程逻辑的正确性验证，即服务流验证的内容非常广泛， 总的来说包括下面四个方面： 是否合乎规定的语法； 是否会导致错误的执行( 任务路由) ； 是否合乎执行时期的语义，即与企业业务过程的目标是否一致； 是否可能在现有的软、硬件资源下执行。 在第二章论文还将更具体地对这四个方面进行分析。 w e b 服务组合验证是w e b 服务组合的投入使用前的一个必要步骤，它能提 前发现服务组合中存在的问题，以确保投入使用的服务组合能正常工作，从而提 高服务执行的成功率和用户满意度，它是企业构建正确的基于s o a 的应用系统 要保障，是s o a 系统真正步入实用阶段前必须要解决的问题。 1 2 国内外研究现状 目前w e b 服务及其组合的形式化描述和验证是w e b 服务中一个重要的研究 方向，现有的许多w e b 服务及其组合描述语言都是半形式化的，容易出错和不 容易检测，正确性难以保证，需要有形式化的方法来验证w e b 服务组合模型是 否正确。模型的正确性是指模型结构上的正确性，即是安全、有界、无死锁等， 在下文中会有更具体的描述。 w e b 服务组合可以使用不同的形式化方法描述和验证。一般而言，当前研究 多集中于使用p e t r i 网、自动机理论和进程代数( p r o c e s sa l g e b r a ) 这三种形式化 方法来进行w e b 服务组合验证【2 5 】。 p e t r i 网具有直观的图形表示方式和丰富的形式化语义，能够自然地描述并 发、同步和资源竞争等系统特性，适合描述w e b 服务的动态行为，所以比较适 6 浙江大学硕士学位论文第1 章绪论 合验证w e b 服务的运行状态。文献【8 】详细介绍了w e b 服务的p e t r i 网建模过程： 用两个库所和一个变迁表示一个w 曲服务，第一个库所用来接受w e b 服务的输 入信息，变迁代表制定的w e b 服务操作，第二个库所用来输出操作所产生的结 果。文献【2 9 】提出使用扩充的p e t r i 网明巳网来验证流程是否有死任务和流程的正 确完成性。 基于有限自动机的w e b 服务组合的建模与验证也有不少研究成果文献 2 0 1 1 2 1 脾1 给出一套技术和工具( g u a r d e da u t o m a t a 、p r o m e l a 语言、s p i n 模型检测 器) 以及一个完整的系统分析和验证组合w e b 服务的方法，可方便地使用工具分 析组合w e b 服务的正确性。文献t 1 2 l 为简化并自动化组合w e b 服务验证，提出一 种基于扩展有限自动机验证组合w e b 服务的方法。该方法不但可以验证组合 w e b 服务是否满足系统需求，还可以验证组合w e b 服务运行过程是否有逻辑 错误。 进程代数使用通信作为进程间互相作用的基本手段，所以非常适合用来描述 和验证并发系统。尤其似乎p i 演算不仅可以传递变量和值，还可以传递通道名。 这使p i 演算具有建立新通道的能力。所以它特别适合用来描述分布式松耦合的 并发系统。文献【l l l 使用p i 演算来建模w e b 服务组合，并使用m w b 自动化工具 来验证w e b 服务组合系统存在的死锁、活锁、状态不可达到等问题。 由于p i 演算比较抽象，图形表达能力较弱，所以不适合直接来描述服务组 合。当前的研究主要集中于p i 演算和w e b 服务元素的对应关系、建模规则等方 面。但如何对建模完成的服务组合进行死锁、同步等问题的检测还处于起步阶段。 大多数研究人员都采用m w b 等模型工具进行演算，但m w b 等工具自动化程度 不高，问题描述不清，而且难以和服务组合定义工作结合，这些问题使p i 演算 在服务组合验证领域还停留在理论研究阶段。 1 3 研究背景与研究内容 本文工作是国家科技支撑计划 现代服务业共性技术支撑体系与应用示范工 程 重大项目一现代服务业服务基础技术研究( 2 0 0 6 b a h 0 2 a 0 1 ) ) 的一部分。本 项目旨在研究和攻克一系列关键性现代服务业共性服务基础技术，形成基础支撑 系统和平台，为多种典型应用和服务提供基础运行支撑和开发管理支持。项目由 浙江大学( 具体参加单位为浙江大学计算机科学与技术学院c c n t 实验室) 牵 头，联合阿里巴巴研究院、中国卫通网络通信有限公司、中国科学院软件研究所、 西安交通大学五家共同承担研制。在该项目中，浙江大学主要负责理论研究、核 心技术攻关和平台研发。而本文工作则是核心服务层理论研究的内容之一。核心 服务层的主要研究内容包括服务的描述与建模、服务发现与匹配、服务流程与验 7 浙江大学硕士学位论文 第1 章绪论 证、服务监控与执行等问题。 论文围绕w e b 服务组合建模和验证问题展开研究，针对w e b 服务组合及业 务流程的特点，分析当前w e b 服务组合验证的研究现状，研究基于p i 演算的服 务流验证方法。并在w e b 服务组合平台j t a n g f l o w - s 上，实现了流程组合验证 模块，以协助设计人员在服务组合流程实施前对其进行分析和验证。 论文的主要研究内容包括：对w e b 服务组合的关键技术及验证方法进行了 分析和研究；对p i 演算进行研究，使用p i 演算代数作为流程建模、分析和验证 的工具：明确组合流程验证的功能需求，设计一个组合流程验证模型：在w e b 服务组合平台j t a n g f l o w - s 上，采用e c l i p s e 插件开发的方式开发组合流程建模 和验证工具。 第3 章基于p i 演算的 摄务流模型转换 第4 章基于p i 演算的 服务流验证算法 图1 4 论文组织架构 如图1 4 所示，论文组织架构如下： - 第二章问题定义与典型方法。介绍服务流验证的基本理论和相关技术，比 较几种热门验证技术，为基于p i 演算的服务流验证模型的设计及工具的实 现提供理论基础和技术背景。 - 第三章基于p i 演算的服务流模型转换。介绍p i 演算的基本理论和s f d l 服 务组合描述语言的元模型，并且将两者相结合提出s f d l 的p i 演算建模方法， 包括将s f d l 模型转换成p i 演算表达式的算法。 - 第四章基于p i 演算的服务流验证算法。首先介绍服务流验证的内容，即流 程中状态的可到达性、流程的可终结性、流程的活性、死锁和活锁等问题， 并结合第三章s f d l 的定义给出其形式化定义。然后结合实例，讨论了各种 问题的如何使用p i 演算推演算法进行识别和验证。最后本章讨论利用m w b 等工具进行自动化验证的优缺点，并提出改进方法。 - 第五章基于p i 演算的服务流验证原型系统实现。在本文提出的验证模型的 8 浙江大学硕士学位论文第1 章绪论 基础上，本章着重从模型的主要模块、设计思路及模型框架等方面全面介绍 该验证模型，本章在e c l i p s e 平台上实现了w e b 服务组合流程验证工具。 第六章总结与展望。总结论文的主要工作，并在此基础上分析了开发的业 务流程验证工具的缺点和不足，对下一步的研究工作提出了展望。 1 4 本章小结 本章力求读者对本文设计的服务组合及其验证技术有一个大致的了解，并对 本文的研究背景和研究内容做了阐述。本章首先介绍了s o a 的概念、发展和现 状，并重点阐述了w e b 服务的技术框架和服务组合的相关技术。然后介绍了服 务组合验证的必要性、定义等，并阐述了目前服务组合验证技术的研究状况。最 后本章介绍了论文的研究背景和内容组织结构。 9 浙江大学硕士学位论文 第2 章问题定义与典型方法 第2 章问题定义与典型方法 本章首先对w e b 服务组合进行分类，提出服务流的定义，讨论当前流行的 三种w e b 服务组合验证的方法。同时详细分析基于p e t r i 网、自动机理论和进程 代数的形式化方法验证方法，总结这三种验证方法的优缺点，为本文下一步提出 基于p i 演算的服务流验证方法提供基础。 2 1w e b 服务组合及服务组合验证问题定义 图2 1w e b 服务组合的研究内容 如图2 1 所示，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 曲服务组合目前还没有一个统一的定义。文酬6 】认为w e b 服务组合是指 单个w e b 服务无法满足用户需求时，将若干个w e b 服务进行有机组装，形成大 粒度的具有内部流程逻辑的组合服务的过程。文献 7 1 认为w e b 服务组合是利用 i n t e m e t 上分布的现有的w e b 服务，根据用户的应用需求，自动地选择合乎需要 的服务，在服务组合支撑平台的支持下，按照一定的规则协同完成服务请求。 人工设计完成的流程可能存在众多问题，而服务组合验证是服务流程进入实 用前的必要过程，国内外研究人员对其展开了广泛的研究。上一章已经将将w e b 服务组合验证问题分为两大类：一是验证服务组合内部服务流程逻辑的正确性； 二是验证服务组合中各服务间的兼容性。本文的重点是前一部分。这里简单介绍 一下第二类验证问题的研究现状，具体可见文献 1 8 】【3 7 1 。在文献 6 】中描述了如何用 p i 演算验证服务组合中服务问的行为兼容性。其主要过程是将服务行为兼容性的 1 0 浙江大学硕士学位论文第2 章问题定义与典型方法 验证过程转换成并行进程的推演过程，借助p i 演算的操作语义和自动推演能力 实现自动验证。 下面具体分析服务流验证的问题定义。在上文中已经提到，服务流验证和工 作流验证类似，可分为四个方面： 是否合乎规定的语法； 是否会导致错误的执行( 任务路由) ； 是否合乎执行时期的语义，即与企业业务过程的目标是否一致： 一是否可能在现有的软、硬件资源下执行。 其中是否合乎规定的语法是一个重要的验证项目，但是比较简单，一般只需 检查流程描述文件是否符合流程定义语言的s c