（控制理论与控制工程专业论文）基于进程代数的web服务编排方法及其类型理论研究.pdf

一夕 上海人学博士学位论文 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特另j , d n 以标注和致谢的地方外，论文中不包含其他人己发表 或撰写过的研究成果。参与同一工作的其他同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示了谢意。 签名矢望堕日 本论文使用授权说明 期：三：三星：呈：! ! 本人完全了解上海大学有关保留、使用学位论文的规定，h i j ：学 校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学校可 ( 保密的论文在解密后应遵守此规定) 签名：纽导师签名：鼍；型兰主h 期：2 华3 矗 上海大学工学博士学位论文 基于进程代数的w e b 服务编排方法 及其类型理论研究 作者 导师 专业 学位 黎升洪 缪淮扣教授 控制理论与控制工程 工学博士 上海大学计算机工程与科学学院 二o o 九年七月 上二海大学博士学位论文 s h a n g h a iu n i v e r s i t yd o c t o r a ld i s s e r t a t l 0 n r e s e a r c ho nt h em e t h o do f w e bs e r v i c ec h o r e o g r a p h y a n di t st y p et h e o r y b a s e do np r o c e s s a l g e b r a b y l is h e n g h o n g s u p e r s o rp r o f e s s o rm i a oh u a i k o u m a j o r d e g r e e c o n t r o lt h e o r ya n dc o n t r o le n g i n e e r i n g d o c t o ro ft e c h n o l o g y j u l y2 0 0 9 s h a n g h a i ，p r c h i n a 上海人学博士学位论文 摘要 面向服务计算是下一代基于瓦联网的全新软件体系结构。它具有分布、共 享、健壮、可扩展、可移植、互操作等特性。这些特性主要来自服务的互操作 特性和复合特性。面向服务计算目前主要实现方式是基于w e b 服务。w e b 服务 是分布、独立的代码片断，通过相互交换信息来完成一个特定任务。不同于传 统的软件组件，w e b 服务可以通过互联网进行交互。w e b 服务的实现得益于 w e b 服务标准的发布，主要是三个基础协议：内容使用格式无关的x m l ；网 络资源的命名使用u r i ；消息的传递使用h t t p 或s o a p 。w r e b 服务标准包括： w e b 服务接口描述w s d l 、语义w e b 服务等。然而，w e b 服务实现复杂功能 的关键是将功能单一的多个w e b 服务复合为功能复杂的w e b 服务。因此，w e b 服务中关键技术是w e b 服务复合。目前w 3 c 等组织主要有两种候选方案： w s b p e l 和w s c d l 。w s c d l 是交互描述语言，称为w e b 服务编排 ( c h o r e o g r a p h y ) 。它从全局的角度来看w e b 服务复合，通过w s c d l 描述可以 保证多个w e b 服务交互的无死锁、活锁、公平等性质。其w o r k u n i t 提供模块 复用功能。w s c d l 的主要特色包括w o r k u n i t 和基于信息对齐交互。w s b p e l 称为w e b 服务编f l ；l j ( o r c h e s t r a t i o n ) 执行语言。它是从一个参与者的角度来实现 w e b 服务的复合功能。 w e b 服务标准中存在定义不严谨的情况，即没有给出w s b p e l 和w s c d l 的严谨语义，其结果可能导致几个简单w e b 服务间复合存在不兼容的情况，这 样就有必要采用严密的形式化方法来描述验证w e b 服务编排复合性质。 进程代数是用代数方法对分布与并发系统进行研究。进程是进程代数的元 素，进程代数可以通过给定公理和复合算子的方法来定义。常见复合算子包括： 顺序、并行、随机选择、递归演算。这样就可以用功能强大的代数规格说明来 描述系统，并可以验证系统性质。 本文以w e b 服务编排复合方法为研究对象，以w e b 服务编排复合为目标， 研究基于进程代数的w e b 服务编排复合关键方法和技术。主要贡献与创新如 下： 1 ) 提出了基于进程代数的w e b 服务( p r o c e s sa l g e b r af o rw e bs e r v i c e p a 4 w s ) 形式化模型，给出了p a 4 w s 的语法模型、语义模型、类型理论、子 类型关系和递归类型的子类型关系四部分。 2 ) p a 4 w s 语法模型中，和已有的研究成果相比，除常规的输入、输出等 基本交互外，在借用服务( 会话) 通道概念描述基本交互基础上，新增w o r k u n i t i 二海大学博十学位论文 算子。会话是对无限制、复杂交互进行封闭的较常规抽象方法，它的引入保证 了服务中的数据无关性和数据能够被隐式创建；w o r k u n i t 算子的引入可方便地 描述w e b 服务交互的异步性质。更重要的是，就我们所知，这是首次借助 w o r k u n i t 算子形式化描述了w e b 服务编排中基于信息对齐的交互。 3 ) 在p a 4 w s 语义模型中，定义了其结构化小步操作语义，并给出p a 4 w s 自由变量、受囿变量、结构化同余关系的定义、相关的代数性质及其证明。 4 ) 在类型理论中，基于基础公理的类型描述框架，给出p a 4 w s 类型环境 推演构造规则、值推演规则和类型推演规则等理论体系。基于结构归纳法和规 则归纳法等证明论方法给出p a 4 w s 类型理论的健全性检查、进程项同余关系 一致性和进程项归约关系一致性等相关性质证明。 5 ) 在子类型关系和递归类型的子类型关系部分，基于( 逆像) 良基归纳法和 余归纳法，证明了带递归算子的子类型关系与正则树子类型是一致的。 6 ) 基于i a v a c c 和v i z g r a p h ，开发了简化版p a 4 w s 到执行树的图形化表示 j a v a 原型系统，执行树图形化表示采用d o t 语言。 最后，通过一个电子商务实例建模和基于信息对齐的交互建模来说明 p a 4 w s 带来的优点。 关键词：w e b 服务编排复合，进程代数，结构化操作语义，类型理论，子 类型关系，递归类型，余归纳法，仿真器。 上海大学博士学位论文 a b s t r a c t s e r v i c e o r i e n t e dc o m p u t i n g ( s o c ) i sn e w g e n e r a t i o ni n t e m e t - b a s e da r c h i t e c - t u r e s o ch a sm a n yc h a r a c t e r i s t i c si n c l u d i n gd i s t r i b u t a b i l i t y , s h a r e a b i l i t y , r o b u s t n e s s ， e x p a n s i b i l i t y , p o r t a b i l i t y , i n t e r o p e r a b i l i t y , e r e a l lo ft h e s ec h a r a c t e r i s t i c sa r ef r o m i n t e r o p e r a b i l i t ya n dc o m p o s i t i o no fs e r v i c e s t h ep r i m a r yi m p l e m e n t a t i o no fs o ci s b a s e do nw e bs e r v i c e s ( w s s ) w s sa r ed i s t r i b u t i n ga n di n d e p e n d e n ts n i p p e t sw h i c h s o l v eas p e c i f i ct a s kb yi n t e r a c t i o na m o n gw s s ，w h e r ew s si n t e r a c tw i t he a c ho t h e r t h r o u g hi n t e r n e t i ti sd u et ot h es t a n d a r d so fp r o t o c o ls t a c ko fw s ，w h e r e x m l - b a s e dc o n t e n t sa r ei n d e p e n d e n to ft h e i rf o r m a t ，n e t w o r kr e s o u r c e sa r eu r i s ， a n dm e s s a g e sa r es e n ta n dr e c e i v e db yh t t po rs o a p t h es t a n d a r d si n c l u d e w s d la n do w l - s ，b u tt h ec r u c i a li s s u ei sc o m p o s i t i o no fw s st h a tp r o v i d e sa v a l u e - a d d e dw sb ya ne x e c u t i o no fs i m p l ew s s t h ec a n d i d a t es t a n d a r d si nw 3 c a r ew s c d la n dw s - b p e l w s c d li sa ni n t e r a c t i v ed e s c r i p t i o nl a n g u a g e ，c a l l e d c h o r e o g r a p h y , w h i c hd e p i c t st h ec o m p o s i t i o no fw s sf r o mg l o b a lv i e wi no r d e rt o g u a r a n t e et h ep r o p e r t i e s ，f o re x a m p l e ，s a f t y n e s s ，l i v e n e s sa n df a i m e s s t h ew o r k u - n i to fw s c d lp r o v i d e sr e u s a b l ef u n c t i o n t h em a i nc h a r a c t e r i s t i c so fw s c d l i n c l u d ew o r k u n i ta n di n t e r a c t i o nb a s e di n f o r m a t i o na l i g n m e n t ( i b i a ) w s b p e l i sa ne x e c u t i o nl a n g u a g e ，c a l l e do r c h e s t r a t i o n ，f o rt h ec o m p o s i t i o no fw s sf r o mo n e o f p a r t i c i p a n t sv i e w t h e r ea r en o tr i g o r o u ss e m a n t i c sf o rt h e s ec a n d i d a t es t a n d a r d s ，w h i c hw i l ll e a d t oi n c o m p a t i b l ea m o n gw s s ，f o re x a m p l e ，s e v e r a ls i m p l ew s sc a nn o tb ec o m p o s e d f o rac o m p l i c a t e dt a s k i ti sn e c e s s a r yt h a tf o r m a lm e t h o d sa r ee n g a g e di nt h ed e s c r i p t i o na n dv e r i f i c a t i o no ft h ec o m p o s i t i o no f w s s p r o c e s sa l g e b r ai sar e s e a r c ho nd i s t r i b u t i n ga n dc o n c u r r e n ts y s t e mb yu s i n g a l g e b r a i cl a w s b a s i c a l l y , ap r o c e s si sa ne l e m e n to fp r o c e s sa l g e b r a p r o c e s sa l g e b r a c a nb ed e f i n e db ya x i o ml a w sa n dg i v e nc o m p o s i t eo p e r a t o r s ，f o re x a m p l e s ，s e q u e n c e ，c o m p o s i t i o n , s u m m a t i o na n dr e c u r s i v eo p e r a t o re t c ap o w e r f u la n dd e l i c a t e s p e c i f i c a t i o no fs y s t e mc a nb ee x p r e s s e d , a n ds y s t e mp r o p e r t i e sc a nb ev e r i f i e d t h i st h e s i sr e s e a r c h e so nc r i t i c a lm e t h o d sa n dt e c h n o l o g i e so fc o m p o s i t i o no f w s s b ym e a n so fp r o c e s sa l g e b r a ，w h e r et h eo b j e c t sa r et h em e t h o d so fc o m p o s i t i o n o fw s s ，a n dt h et a r g e t sa r et h es o l u t i o no ft h ec o m p o s i t i o no fw s s h e r ea r et h e i i i 上海大学博士学位论文 m a i nc o n t r i b u t i o n sa n di n n o v a t i o n 1 ) af o r m a lf r a m e w o r ko fc h o r e o g r a p h yo fw s s ，p r o c e s sa l g e b r a f o 厂w e bs e r - v i c e ( p a 4 w s ) ，i sp r o p o s e db a s e do np r o c e s sa l g e b r a t h es y n t a x ，s e m a n t i c s ，t y p e t h e o r y , s u b t y p i n ga n dr e c u r s i v es u b t y p i n go fp a 4 w s a r ep r e s e n t e d 2 ) t h ei n t e r a c t i v ee l e m e n t si nt h es y n t a xo fp a 4 w sh a v es p e c i a l l yw o r k u n i t o p e r a t o rw i t hs e r v i c e ( s e s s i o n ) c h a n n e lb e s i d e st h ec o m m o ni n p u ta n do u t p u ti n t e r - a c t i o nc o m p a r i n gw i t ht h el i t e r a t u r e t h en o t i o no fas e s s i o ni sam o r ec o n v e n i e n t a b s t r a c t i o nm e c h a n i s mf o re n c l o s i n ga r b i t r a r i l yc o m p l e xi n t e r a c t i o n sb e t w e e np e e r s ， w h i l eas e s s i o nl e a d st od a t a - i n d e p e n d e n ta n dd a t ac a nb ec r e a t e di m p l i c i t l y t h e c o n c u r r e n ta n da s y n c h r o n o u sp r o p e r t i e so fi n t e r a c t i o n so fw s sc a l lb ec o n v e n i e n t l y d e p i c t e db yw o r k u n i t m o r e o v e r , t h ei b i ai sf i r s t l ym o l d e db ym e a n so fw o r k u n i t a sm u c ha sw ek n o w 3 ) i nt h es e m a n t i c so fp a 4 w s ，t h ed e f i n i t i o no fs m a l ls t r u c t u r a lo p e r a t i o n a l s e m a n t i c s ，f r e ev a r i a b l e s ，b o u n dv a r i a b l e s ，a n ds t r u c t u r a lc o n g r u e n c ea r eg i v e na n d p r o p e r t i e so fa l g e b r a i cl a w sa r es h o w n 4 ) i nt y p et h e o r y , w ep r e s e n td e d u c t i o nr u l e ss u c ha sv a l u e s ，e n v i r o n m e n t sa n d i t e m so fp a 4 w sb a s e do nf r a m e w o r ko ft h ea x i o mo ff o u n d a t i o n w es h o wt h e p r o p e r t i e so ft h et y p et h e o r y , s u c ha ss a n i t yc h e c k , s u b j e c tc o n g r u e n c ea n ds u b j e c t r e d u c t i o nb ym e a n so ft h es t r u c t u r a li n d u c t i o na n dt h er u l ei n d u c t i o n 5 1w ed e f i n es u b t y p i n gr e l a t i o n s h i pa n ds h o wr e c u r s i v es u b t y p i n gc o n s i s t e n t w i t hn o r m a ls u b t y p i n gi np a 4 w s b ym e a n so f ( i n v e r s ei m a g e ) w e l l - f o r m e di n d u e - t i o na n dc o i n d u c t i o nw h e nt h es u b t y p e so fp a 4 w sa r er e g u l a rt r e et y p e s 6 ) ag u i p r o t o t y p es y s t e mi sd e v e l o p e dt h a tt r a n s l a t e st h es y n t a xo fs i m p l i f i e d p a 4 w st oe x e c u t i o nt r e s su s i n gd o tl a n g u a g ea n dt o o l so f j a v a c c ，v i z g r a p h y f i n a l l y , t h eb e n e f i t so fp a 4 w sa r ee x e m p l i f i e db ya ne - b u s i n e s sa n di n t e r a c t i o n b a s e di n f o r m a t i o na l i g n m e n t k e yw o r d s ：c o m p o s i t i o no fw e bs e r v i c ec h o r e o g r a p h y , p r o c e s sa l g e b r a ， s t r u c t u r eo p e r a t i o n a ls e m a n t i c s ，t y p et h e o r y , s u b t y p i n g ，r e c u r s i v et y p e ，c o i n d u c t i o n ，s i m u l a t o r i v 上海大学博士学位论文 目录 摘要i a b s t r a c t i i i 第1 章绪论1 1 1 研究背景1 1 2 研究现状2 1 2 1 进程代数元理论2 1 2 2 相关工作3 1 3 研究意义5 1 4 论文主要研究内容与结构安排6 1 4 1 主要研究内容z6 1 4 2 总体思路与内容安排8 第2 章背景知识和相关工作一11 2 1 代数概论11 2 2 进程代数1 3 2 2 1 进程代数语法1 3 2 2 2 进程代数语义1 3 2 2 3 进程代数类型理论1 4 2 2 4 进程代数等价理论15 2 3 基于归纳的证明方法1 6 2 3 1 结构归纳法原理1 6 2 3 2 良基归纳法原理1 7 2 3 3 规则归纳法1 8 2 3 4 余归纳法。1 9 2 4w e b 服务复合中形式化方法1 9 2 4 1w e b 服务协议栈1 9 2 4 2 形式化方法在w e b 服务复合中应用2 1 2 5 小结2 2 第3 章p a 4 w s 的语法和语义2 3 3 1w s c d l 概述2 3 3 2p a 4 w s 语法2 7 3 2 1 p a 4 w s 语法。2 7 3 3p a 4 w s 语义。2 9 3 4 实例建模3 4 v 上海大学博士学位论文 3 5 基于p a 4 w s 的w s c d l 交互模式建模描述3 6 3 6d 、结3 7 第4 章p a 4 w s 的类型理论3 9 4 1 类型定义4 0 4 1 1 类型扩展规则4 3 4 2p a 4 w s 类型推理规则4 4 4 2 1 良构类型环境构造规则4 4 4 2 2 值类型规则4 6 4 2 3 类型推理规则4 7 4 2 4 对偶规则5 0 4 3 类型例子5 l 4 4 类型规则的性质5 2 4 5 相关工作5 4 4 6 小结5 5 第5 章子类型关系与递归类型的子类型关系5 7 5 1p a 4 w s 中的子类型关系一5 7 5 2 递归类型的子类型关系性质5 8 5 2 1 树类型的子类型关系性质6 1 5 2 2 递归类型的子类型关系性质分析6 5 5 3 最大不动点算法6 7 5 4 进一步讨论6 7 5 5 小结6 9 第6 章p a 4 w s 到状态迁移图转换的实现。7 1 6 1 引言7 1 6 2 状态迁移图的d o t 语言表示方法7 1 6 3p a 4 w s 模型转换成状态迁移图模型7 3 6 3 1 模型转换的整体架构7 3 6 3 2 主要类图和对应的数据结构7 5 6 3 3 主要算法和输出格式7 8 6 4 一个运行实例8 0 6 5d 、结8 3 第7 章结束语。8 7 7 1 本文主要贡献8 7 7 2 迸一步工作8 8 v i 上海大学博士学位论文 附录a ：p a 4 w s 语法和语义8 9 附录b ：p a 4 w s 类型理论9 l 附录c ：类型系统证明9 5 参考文献1 0 3 攻读博士学位期间发表的论文1 1 3 攻读博士学位期间参与的课题11 4 致谢1 1 5 l 上海人学博十学位论文 卜海人学博十学位论文 1 1 研究背景 第1 章绪论 面向服务计算( s e r v i c e - o r i e n t e dc o m p u t i n g ，s o c ) 是下一代基于互联网的 全新软件体系结构。在s o c 中将所有功能都定义为服务。这些服务既包括简单、 低级服务，也有将简单低级服务复合形成的高级服务。所有这些服务是自治的， 对外部组件而言，其操作是透明的。这样外部组件无需关心服务如何实现其功 能，而仅仅关心服务调用方法和返回的结果。就是说，服务接口被封装了。 在大多数情况下，无论对本地和远程部件而言，服务接口是均可调用。这 种交互方式可以保证有效调用功能，而不关心底层如何实现连接。 基于s o c 的软件体系结构开发软件【l 】，可为业界带来如下好处： 快速应用集成。 自动化商务过程。 应用访问的多样性，例如，包括固定和移动设备。 s o c 为软件开发带来下列好处： 可重用性。 简单性。 开发高效性。 低耦合性。 s o c 体系结构具备下列优点： 分布性。 可扩展性。 可移植性。 可伸缩性。 健壮性。 s o c 所有这些特性都来自服务的互操作特性和复合特性2 ，3 1 。s o c 目前主 要实现方式是基于w e b 服务【4 ，5 1 。w e b 服务是分布、独立的代码片断。w e b 服 务间通过相互交换信息来求解一个特定复杂任务。不同于传统的软件组件，w e b 服务可以通过互联网进行交互。w e b 服务的实现得益于w e b 服务标准的发布， 主要是三个基础协议：内容使用与格式无关的x m l ；网络资源的命名使用u r i ； 消息的传递使用h t t p 。w e b 服务标准包括：w e b 服务接口描述w s d l 6 1 、语 义w e b 服务 7 1 等。然而w r e b 服务实现复杂功能的关键是将功能单一的多个w e b 上海人学博十学位论文 服务复合为功能复杂的w e b 服务。因此w e b 服务中关键技术是w e b 服务复合 3 1 。目前w 3 c 等组织主要有两种候选方案。w s b p e l 1 5 1 和w s c d l l l 6 ，1 7 1 。 这里w s c d l 是从全局的角度来看w e b 服务复合，它是描述语言，通过 w s c d l 可以避免死锁、活锁等情况发生，w s c d l 称为w e b 服务编排 ( c h o r e o g r a p h y ) ，其w o r k u n i t 提供了模块复用功能是w e b 服务编排的主要特色； w s b p e l 是实现从某个参与者角度出发的w e b 服务复合功能的标准，它是执 行语言，w s b p e l 称为w e b 服务编锘1 ( o r c h e s t r a t i o n ) 。 w e b 服务标准中存在定义不严谨的情况，即没有给出w s b p e l 和w s - c d l 的严谨语义【1 8 1 9 】，其结果可能导致几个简单w e b 服务间复合存在不兼容的情 况，这样有必要采用严密的形式化方法来描述和验证w e b 服务编排性质。给出 w e b 服务编排复合的形式化语义，特别是基于进程代数的w e b 服务复合研究， 本文基于进程代数方法对w e b 服务编排给出形式化描述和对应的类型理论，既 具有理论意义又有现实意义 1 2 研究现状 基于进程代数的w e b 服务编排复合形式化方法研究需要确定研究进程代 数元理论、w e b 服务关键特征与进程代数映射这两个方面。下面从进程代数元 理论和w 曲服务编排形式化建模( 验证) 这两个方面分析与本课题相关的国内 外研究现状。 1 2 1 进程代数元理论 进程代数 2 0 瑚】是用代数方法对分布与并发系统进行研究。“进程代数 一词 由“进程”和“代数”两个词构成。“进程”泛指系统的行为，行为是系统所执 行动作或事件序列的总和，进程代数也被称为离散事件系统。“代数”表示通过 某种代数公理化的方法来研究系统行为。可以通过给定算子和公理的方法来定 义进程代数。进程是进程代数的元素，通过使用公理，我们可以对进程进行顺 序、并行、随机选择、递归演算，用获得的功能强大的代数规格说明书来描述 系统。进程代数可以被认为是形式化语言和自动机经典理论的通用描述1 2 引，它 不着重于语言的识别和生成，而致力于系统规范与行为。 在关键系统设计中，进程代数在形态上夯实理论基础。它提供对规格说明、 验证、实现、测试和其它生命周期关键活动的支持。历史上，a l o n z oc h u r c h 构造了具有顺序算子的l a m b d a 演算【3 0 l ，l a m b d a 演算是和a l a nm t u r i n g 构造 2 上海大学博士学位论文 的图灵自动机具备相同计算能力的两个著名计算模型。8 0 年代初期r o b i n m i l n a 引入并行算子构造了c c s ( ac 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 ) p 1 ，3 引、 c a r h o a r e 同时引入并行算子构造了c s p ( c o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ) 3 3 - 3 5 、r o b i nm i l n e r 在c c s 和c s p 基础上引入进程移动概念构造了p i 演 算f 3 6 3 9 1 ，其对应的工具为m w b l 4 0 1 。目前a s p ( a s y n c h r o n o u ss e q u e n t i a lp r o c e s s e s ) t 4 1 1 和a m b i e n tc a l c u l u s ( 界程演算) 【4 2 删等在理论研究方面具备了更多描 述并发异步系统性质的功能，并有相应工具支持。基于进程代数理论思想的f 群、 h a s k e l l 等函数语言也成为工业界当前编写应用程序的流行语言。 所有这些基于进程代数研究方法中存在一个元理论框架，下面我们简要给 出该元模型框架： 1 ) 语法定义。2 ) 语义研究【4 5 捌】。3 ) 对并发系统的进程代数理论进行研究【5 2 】。 4 ) 互模拟理论 5 3 - 5 5 】。5 ) 类型理论【5 9 1 。6 ) 类型检查算法f 6 0 , 6 1 。7 ) 进程代数的性质 描述。 进程代数系统包括两个部分，不可再分的基本动作部分和基于这些基本动 作的复合算子，通过复合算子提供更抽象、复杂的行为描述。将w e b 服务中基 础、简单的交互对应于进程代数的不可再分的基本动作，对这些简单、基本的 w e b 交互动作进行顺序、并发、随机分支、递归等复合操作来提供w e b 服务复 合描述。基于进程代数w 曲服务复合研究的优点包括：可复合性、互模拟性、 安全性等时态性质和仿真性，其具体含义在2 4 2 节解释。 1 2 2 相关工作 ( 1 ) 基于进程代数的w e b 服务复合 1 ) c a s p i s 演算模型 c a s p i s 似c a l c u l u so f s e s s i o n sa n dp i p e l i n e s ) 是基于进程代数的w 曲服务形 式化模型【6 2 】。与其它进程代数相同的是它具有并发、分支、重复和受囿等算子。 不同于通常的进程代数，它引入会话概念，包括会话创建、会话内通信和会话 间通信；它还引入c l o s e 原语来取消一个会话的执行。闭包应答( c l o s u r en o t i f i c a t i o n ) 是c a s p i s 特有的原语，它用来处理( 异常或程序的) 会话终结。c a s p i s 通过模式匹配来强化服务交互。但是c a s p i s 没有讨论类型理论，也没有引入 工作单元建模。 上海人学博十学位论文 2 ) 全局演算模型 c a r b o n e ，h o n d a 等人提出全局演算( g l o b a lc a l c u l u s ) 来描述w e b 服务编排， 局部演算( l o c a lc a l c u l u s ) 来描述w 曲服务编制【6 3 】。两个演算均引入会话概刽6 1 硎，较好地刻画了基于网络交互的性质，即一个服务通道中可以有多个会话通 道。同时，基于参与者位置信息( 文章中称为线索( t h r e a d ) ，提出从全局演算到 局部演算的映射，具体来说，对给定的全局演算标注线索，根据线索提供的位 置信息和转换规则，转换全局演算到局部演算。作者提出了三条约束准则：可 连接性( c o n n e c t e d n e s s ) 、良线索性( w e l l t h r e a d e d n e s s ) 和一致性( c o h e r e n c e ) 。 全局演算模型优点是引入通道和会话的概念，较好的刻画了交互性质。缺 点是没有对w s c d l 中的复用要素进行建模，即没有对w o r k u n i t 进行建模。 3 ) s o c k 演算模型 g u i d i 等人提出了s o c k 演算模型【6 5 6 6 s o c k 模型是针对整个w 曲服务的 共性部分提出的一个演算模型，其分为服务行为、服务引擎和服务系统三个演 算。服务引擎演算和服务系统演算类似界程演算中的系统演算，其抽象级别更 高。在服务行为演算中，基本交互模式有基于单消息的单向发送、单向接收和 基于两个消息的请求应答、不断请求应答四种模式。服务行为演算具备多数 进程代数所具有的算子，例如顺序、并行、随机选择等。由于有更高级别的系 统行为描述，它具备高级别系统行为复合运算功能，这是该文章思想的体现。 然而，其将“发送应答”视为原子语句的方法不利于性质验证。 4 ) 其它基于进程代数的方法 北京大学裘宗燕教授等6 倘明构造了一个进程代数系统，描述了w e b 服务编 排，并根据w e b 服务编排中的角色信息，提出相应规则实现从w e b 服务编排 到w e b 服务编制的映射。 何积丰教授等人应用c s p 对w e b 服务性质进行了建模和验证【7 0 1 ，文献 7 1 】 使用c s p 作为中间描述，实现了模型检查功能。其同样没有考虑复用功能( 工 作单元) 。 苏建文教授等对w | e b 服务编排应该具备的性质进行了阐述1 7 2 ，其对全局和 局部消息及其交互进行了描述。 文献【7 3 】基于互模拟方法对w e b 服务替换性进行验证，国内也有人直接使 用p i 演算对w 曲服务进行建模7 4 】，但没有考虑工作单元，也没有使用服务通 道和会话通道概念。 4 卜海人学博十学位论文 文献 7 5 7 8 均使用进程代数对w e b 服务建模和性质验证的进行应用。 ( 2 ) 基于语义w e b 的w e b 服务复合 文献【7 9 8 1 】基于语义w e b 8 2 ，8 3 1 ，其优点是可以利用语义w 曲来描述w e b 服务复合，并利用语义w e b 引擎来实现w e b 服务复合。缺点是语义w e b 的标 准尚不够完善，自身尚处于发展中。而且w e b 服务编制标准w s c d l 的制定 其思想就是来源于p i 演算等进程代数，应用进程代数来描述w e b 服务编制复 合更自然、简洁。 ( 3 ) 基于自动机或有限状态机( f s m ) 的w e b 服务复合 自动机或f s m 8 4 ，8 5 1 是计算的低级形式，其有成熟工具s p i n 8 6 ，8 刀的支持， 但没有结构同余、互模拟等概念，这使得基于自动机或f s m 的研究方法对复杂 系统的描述和抽象支持不够。 ( 4 ) 基于p e t r in e t 的w e b 服务复合 文献 8 8 9 2 都是基于p e t r in e t 或其变体来描述w e b 服务编排。p e t r in e t 与 进程代数相比，其具备互模拟等价性质，但没有提供高级别抽象运算功能。 ( 5 ) 其它方法 最常见的是将上述多种方法综合来描述w e b 服务复合【8 5 】。文献 9 3 基于消 息状态图对w s c d l 建模。文献【9 4 】应用u m l 对w e b 服务复合进行建模。然 而消息状态图和u m l 自身就没有严谨语义定义。东南大学王红兵教授领导的 团队开发了w s c d l 执行引擎软件，给出了