（计算数学专业论文）web服务组合的形式化建模与相容性分析.pdf

摘要随着w e b 服务技术的研究、发展和应用，众多学者试图寻找w e b 服务组合验证的有效方法，开始运用形式化方法描述w e b 服务组合并对其进行分析。目前国内外有使用进程代数、p e t r i 网、s p i n 等工具来形式化建模、验证w e b服务组合语言，但是他们都存在某些不足，而且多限于探索或者仅停留在理论研究阶段。本文在对现有w e b 服务形式化验证方法的研究基础上，讨论了它们的特点和不足，并详细分析了现在广泛使用的w e b 服务组合语言标准b p e l 4 w s 规范的特性，提出了一套基于p i 演算的b p e l 4 w s 的建模规则，之后深入研究了类型系统理论，提出了一种切实可行的基于类型化p i 演算的w e b 服务组合相容性分析方法。本文的研究内容主要包括三部分：第一部分是对b p e l 4 w s 规范形式化建模的研究，对p i 演算进行了顺序算子的扩充，给出了扩充的语法和操作语义，并用p i 演算的通信并发结构表示b p e l 4 w s 规范的l i n k 结构；基于对b p e l 4 w s规范死路排除d p e 模式的分析，提出了一个完善的解决d p e 问题的p i 演算形式化方法，从而系统地完成了从w e b 服务组合语言b p e l 4 w s 规范到扩充p i 演算的映射；第二部分是对类型系统的研究，我们区分了通道的输入输出能力，将类型互模拟关系扩充到了区分传输能力的通道类型上，并给出了相关性质和定理的证明；我们给出了类型互模拟和子类型的关系，重新定义了类型上下文环境，给出了进程类型定义良好的推理规则，最后定义了类型化p i 演算的规约语义。第三部分在前面两部分研究的基础上，用类型化p i 演算对b p e l 4 w s 描述的w e b 服务组合系统做了形式化表示，提出了基于类型化p i 演算的服务组合相容性检测算法，最后给出了一个银行贷款审批系统的完整检测实例，说明利用该算法检测服务组合系统相容性的可行性。关键词：b p e l 4 w s ，p i 演算，类型系统，相容性分析a b s t r a c tw i t ht h er e s e a r c h ，d e v e l o p m e n ta n da p p li c a ti o no fw e bs e r v i c et e c h n o l o g y ，s o m es c h o l a r ss t a r tt ol o o kf o rv a r i o u sv a li dt e c h n i q u e sf o rt h ev a l i d a t i o no fw e bs e r v i c ec o m p o s i t i o n ，h e n c et h e yb e g i nt om a k eu s eo ft h ef o r m a lm e t h o dt om o d e la n da n a l y s ew e bs e r v i c ec o m p o s i t i o n a tp r e s e n t ，t h ed o m e s t i ca n df o r e i g nr e s e a r c h e r su s et o o l sl i k ep r o c e s sa l e b r a s ，p e t r i n e t ，s p i nf o rf o r m a ls p e c i f i c a t i o na n dv e r i f i c a t i o no fw e bs e r v i c ec o m p o s i t i o n 。p r o g r a m h o w e v e r ，t h e yh a v ec e r t a i nd e f i c i e n c i e s ，a n df u n d a m e n t a li fs t a yi nt h es t a g eo fe x p l o r a t i o na n dt h e o r e ti c a lr es e a r c h b a s e do nt h er e s e a r c hi n t op r e s e n tw e bs e r v i c ef o r m a li z a t i o nc o n f i r m a t i o nm e t h o d s ，t h i sp a p e ra n a l y s e st h e i rc h a r a c t e r i s t i c sa n dt h ed e f i c i e n c i e s ，p r o b e si n t ot h ea n a l y s i so fb p e l 4 w ss p e c i f i c a t i o n ，w h i c hi sw i d e l yu s e df o r w e bs e r v i c ec o m p o s i t i o n ，a n dd e v e l o p sam o d e l i n gr u l ef o rt r a n s f o r m i n gb p e l 4 w st op ic a l c u l u s t h r o u g ht h ei n t e n s i v er e s e a r c hi n t ot y p es y s t e m ，t h i sp a p e rp r o p o s e sap r a c t i c a la n df e a s i b l em e t h o df o rt h ea n a l y s i so fw e bs e r v i c ec o m p o s i t i o nc o m p a t i b i l i t y ，b a s e do nt y p e dp ic a l c u l u s t h ec o n t e n to ft h i sp a p e rm a i n l yc o n s i s t so f3p a r t s ：i nt h ef i r s tp a r t ，w em a k eas t u d yo ft h em o d e li n gb p e l 4 w sw i t hf o r m a lm e t h o d w ep r e s e n tt h eg r a m m a ra n dm a n i p u l a t i n gs e m a n t i co fe x p a n d i n gt h ep ic a l c u l u sw i t hs e q u e n c eo p e r a t o ra n dm a k eu s eo ft h et h ec o n c u r r e n tc o m m u n i c a t i o ns t r u c t u r et or e p r e s e n tt h en o r m a t i v e l i n k ”s t r u c t u r eo fb p e l 4 w s b a s e do nt h ea n a l y s i so ft h ed e a d p a t h e l i m i n a t i o n ( d p e )p a t t e r no ft h eb p e l 4 w s ，w ep r o p o s eam e t h o dt os o l v et h isd p ep r o b le mb yt h eu s eo fp ic a l c u l u s t h u sw es y s t e m a t i c a l l yc o m p l e t et h em a p p i n gf r o mw e bs e r v i c ec o m p o s i t o nl a n g u a g eb p e l 4 w ss t a n d a r dt ot h ee x p a n d e dp ic a l c u l u s t h es e c o n dp a r tm a k e sas t u d yo ft h et y p es y s t e m w ed i s t i n g u i s ht h ei n p u ta n do u t p u ta b i l i t yo ft h ec h a n n e l s ，e x t e n dt h eb i s i m u l a t i o nr e l a t i o no nt y p e st ot h a tc h a n n e lt y p e s ，a n dt h e ng i v et h ep r o o fo fr e l a t e dp r o p e r t ya n da x i o m s w es e tu pt h er e l a t i o nb e t w e e nt h eb i s i m u l a t i o no nt y p e sa n dt h es u b t y p i n g ，r e d e f i n et h et y p ec o n t e x t s ，d e f i n et y p i n gr u l e sf o rw e l l t y p e dp r o c e s s e s ，a n df i n a l l yd e f i n eac o r r e s p o n d i n gr u l ef o rp ic a l c u l u sa d d e dw i t ht y p es y s t e m i nt h et h i r dp a r t ，w eu s et y p e dp ic a l c u l u st om o d e lw e bs e r v i c ec o m p o s i t i o ns y s t e md e s c r i p t e db yb p e l 4 w s b a s e do nt y p e dp ic a l c u l u s ，w ep r o p o s eaa l g o r it h mt oc h e c kt h ec o m p o s i t i o nc o m p a t i b i l i t yo fw e bs e r v i c e a tl a s tw ea p p l yt h ea l g o r i t h mt oac o m p l e t ee x a m i n a t i o no fab a n kl o a na p p r o v a ls y s t e ma n da p p r o v et h a tt h ea l g o r i t h mi sp o s s i b i li t y k e yw o r d s ：b p e l 4 w s ，p ic a l c u l u s ，t y p es y s t e m ，c o m p a t i b i l i t ya n a l y s i si vw e b 服务组合的形式化建模与相容性分析第一章绪论1 1 研究背景w e b 服务是最近几年新提出的面向服务的体系结构，已成为计算机领域研究的热门和重点课题。它在现有的各种异构平台基础上构筑一个通用的与平台无关、语言无关的技术层，具有软件虚拟化、体系结构松耦合化、结构动态构造化心3 的特点。w e b 服务组合语言及其工具还可以作为新型软件开发平台，可以在线动态地将已经存在的一组w e b 服务组合成一个新的实现更复杂功能的w e b 服务。w e b 服务组合的逻辑一般用业务过程建模语言描述，从2 0 0 0 年起，用于w e b 服务组合的几种语言相继出现，包括w s f l 阳3 ，x l a n g ，x p d l ，b p e l 4 w s 4 ，w s c i 5 ，w s c d l ( 6 】，b p m l 7 ( b u s i n e s s p r o c e s sm a r k u pl a n g u a g e ) ，b p s s ( b u s i n e s sp r o c e s ss c h e m as p e c i f i c a t i o n ) 等。目前，b p e l 4 w s 已经逐渐成为业界的标准。用w e b 服务组合语言描述的服务组合流程的可执行程序在实施服务组合的过程中处于核心地位，所以组合服务流程的正确性决定了组合服务是否能正确运行，逻辑错误的组合服务流程将导致被组合的w e b 服务不可正确实施，如果在流程运行之后再更正错误耗费巨大，而且w e b 服务组合实施是在互联网上进行，并不提供测试环境，所以在流程运行之前检验流程的正确性非常重要；尤其对于大规模的w e b 服务组合，依靠服务组合者手工判断流程的组合正确与否也并不是一件轻而易举的事情；并且w e b 服务组合的发展趋势是在i n t e r n e t 上动态的发现和绑定w e b 服务，这是最符合实际需要的方式一随时随地在网上动态的发现、组合服务实现自己需求的业务流程，这种情况下检查w e b 服务是否符合绑定需求、检查w e b 服务是否与w e b 服务组合语言程序相兼容以及检验对业务w e b 服务被u d d i 中具体服务替换后所形成的w e b服务组合是否相容特别重要。所以我们必须在w e b 服务组合实施之前检验w e b 服务组合流程的正确性、无死锁性等问题；在w e b 服务被调用之前验证其与服务组合相容性的问题，如果不相容，需要重新去发现符合需求的服务，然后再绑定执行。并且我们还可以在实际的应用中去促进w e b 服务组合语言规范的完善与发展。硕士学位论文到目前为止，在系统地评估w e b 服务组合语言的能力和建立w e b 服务组合形式化分析与验证方面，还没有明显的努力田1 。有关b p e l 4 w s 的表达性、完备性、正交性，以及用形式化的方法来研究组合w e b 服务的流程的正确性、服务的相容性、服务的替换等等，还未被系统研究，甚至用形式化的方法来自动生成b p e l 4 w s 程序的方法还没有被研究。1 2 研究现状和发展采用形式化方法研究w e b 服务组合语言，如使用有限状态自动机、p e t r i n e t 、进程代数等；提出形式语义、描述及分析w e b 服务组合语言的性质，是近年来的一个趋势凹儿1 0 儿1 2 1 。人们期望能解决类似于下列这样的问题：类似于b p e l 4 w s 的w e b 服务组合语言能否映射到一个安全无死锁的形式化表达式；给出能够检查出b p e l 4 w s t 过程定义中含有不可到达的活动的程序验证方法：带有负的链接出现时的进入条件计算的解决方法；w e b 服务组合语言和其子集是否完备n 引；w e b 服务的相容性、替换性的研究；研究w e b 服务组合语言的语言特征，改进语言规范和其实施等等。通过这些研究验证w e b 服务组合的正确性，改善w e b 服务组合语言的规范和其实施，使其对程序员来说更易用n 副。最近在有关w e b j 报务组合的模型检测和确认方面，正在开展积极的研究。国外：g p i c c i n e l l i 和s l w i l l i a m s 提出了类似c c s 的描述业务流程的演算n4 i ，这个演算比较简单，不能描述像“死路排除( d p e ) ”高级同步模式。加拿大y o r k 大学提出了基于c c s 的b p e 演算n 3 m 儿3 2 3 来描述b p e l 4 w s ，但其缺乏对数据、时间、出错和补偿处理的表示，虽然大大简化了b p e l 4 w s 规范，但不能验证依赖于数据、时间、故障和补偿处理的b p e l 规范行为，其对d p e 问题也没有很好的形式化描述。a n t o n i ob r o g i 等人用传值c c s 来描述w e b j 艮务组合语言n5 f ，并提出了一种程序兼容性、适配性、替换性的解决方案，但是其对通信的数据没有描述，也忽略了d p e 问题的处理，c c s 不能够很清楚的描述如何捕获d p e 问题。s c h r o e d e r 提出了业务流程向c c s 的转换，接着用c w b 作验证n6 1 ，但他研究的业务过程语言较我们研究的w e b j 艮务组合语言要简单的多，尚不清楚该方法是否能用于描述b p e l 4 w s ，特别是用c c s j 何捕获“死路排除”。w e b 服务组合的形式化建模与相容性分析p e t r i n e t 提供了另一种业务流程建模方法n ”，但该方法不适合用作开发b p e l 4 w s 验证工具的基础，对于建模b p e l 4 w s ，标号迁移系统在这方面要强于p e t r i n e t ，因为像“死路排除”高级同步模式不易用p e t r i n e t捕获。s n a k a j i m a 描述了怎样用s p i n x i 具去验证w e b 服务工作流n8 i ，用于描述工作流的语言是w s f l ( w e bs e r v i c ef l o wl a n g u a g e ) ，它是b p e l 4 w s的前身之一，为了能用s p i n 验证，业务过程先要翻译成s p i n 提供的p r o m e l a 规范语言。将业务过程翻译成为验证所用的形式化语言有其缺点：不易将验证工具返回的诊断信息与原来的过程联系起来。使用l t s a _ t 具集和f s p 进程代数的方法n 叼也有同样的弱点。在国内对w e b 服务组合语言进行形式化建模和验证的研究甚少：同济大学有用p e t r i 网来对b p e l 4 w s 进行建模分析乜叫，其没有对死路排除模式进行分析，没有对数据流控制l i n k 作处理，也忽略了对b p e l 4 w s的一些高级属性的建模，并且不利于程序的自动验证、标记源程序的错误及其自动纠正；电子科技大学有用p i 演算来研究w e b h 艮务组合u ，其没有从w e b h 砭务组合语言描述的程序的角度出发来验证流程的正确性，更不用说对死路排除模式、数据流控$ | j l i n k 、故障处理、补偿处理的描述。并且国内尚没有用基于进程代数的形式化方法对w e b 服务组合相容性、适配性、替换性等的研究，国外也甚少。另外值得一提的是，目前在国内外还没有真正的在w e b 服务装配平台中嵌入模型检验工具来对w e b j j 艮务组合语言组合的程序进行形式化的验证，也没有在引擎执行程序时进行服务的相容性分析，而我们的研究工作正是源于这一设想，本文的工作是为它们的实现进行的前期研究。1 。3 本课题的主要工作1 3 1 研究设想和主要研究内容本文的工作是b p e l 4 w s 的自动模型检验的基础，源自湖南省重点科技攻关项目“业务流程装配平台”2 1 在研制和试用中的需求拉动。业务流程装配平台是一个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 ) 架构的w e b 服务半自动组合平台，可完成半自动w e b 服务发现、动态组合、绑定和硕士学位论文执行、监控，应用于跨组织的业务协作、企业应用集成、供应链与e r p 等i n t e r n e t 环境的企业应用。在实际应用环境中，我们发现：w e b 服务组合的正确性、相容性无法在互联网环境中做测试，如何解决组合正确性、相容性验证是一个问题；由于互联网的w e b 服务应用是大规模的，在实际应用中用手工去发现、组合、检查w e b 服务是耗时的、易出错的、甚至是不可行的。我们提倡用更严格的方法分析、验证、改进w e b 服务组合语言程序，辅助b p e l 4 w s 编程，分析服务组合的正确性，因此我们设想在业务流程装配平台中嵌入一个模型检验工具来实现对w e b 服务组合语言的程序作自动的验证，以及往后扩展为w e b 服务有效性、相容性、适配性、替换性等的自动分析工具，作为以后开发一种嵌入w e b h 艮务动态组合分析工具的工作流引擎的基础。本文的主要研究工作是：在对大量国内外进程代数理论、w e b 服务组合建模以及b p e l 4 w s 规范特性进行研究的基础上，我们对p i 演算进行顺序算子的扩充以形式化描述b p e l 4 w s 程序，给出了扩充p i 演算的语法和操作语义，区分了死锁和进程正常结束到达的终止状态的表达，并用p i 演算的通信并发结构表示b p e l 4 w s 规范的1 i n k 结构；基于对b p e l 4 w s 规范死路排除( d p e ) 模式的分析，提出了一个完善的解决d p e 问题的p i 演算形式化方法；采用传名机制分别处理程序化显式抛出错误与非程序化抛出错误的捕获，给出b p e l 4 w s 的出错与补偿处理的p i 演算编码；在以上工作的基础上，系统地完成从w e b j 报务组合语言b p e l 4 w s 规范到扩展p i 演算的映射；最后给出了一个完整的案例说明b p e l 4 w s 程序的建模工作。在研究现有的p i 演算上类型系统成果的基础上，根据w e b 服务的特性，我们对通道的输入输出能力进行了类型定义；在递归类型的基础上，定义了类型的互模拟关系，把互模拟关系扩充到了区分输入输出能力的通道类型上，对相关的性质和定理进行了证明；随后给出了类型互模拟与子类型的关系，以及进程类型定义良好( w e l l t y p e d ) 的推理规则；在以上工作的基础上，我们重新定义了运行时错误和类型化p i演算并发通信规则。在前面两部分研究工作的基础上，我们利用扩充后的类型化p i 演算对b p e l 4 w s 描述的w e b f j 艮务组合系统做了形式化表示，通过对w e b 服务组w e b 服务组合的形式化建模与相容性分析合相容性的讨论，提出了基于类型化p i 演算的服务组合相容( c o m p a t i b i l i t y ) 检测算法，并给出了一个银行贷款审批系统的完整实例建模与规约分析，说明利用该算法检测服务组合系统相容性的可行性。1 3 2 研究的依据我们基于进程代数的理论2 3 m 2 5 m 8 m 9 m4 j ，对p i 演算进行顺序算子扩充后描述b p e l 4 w s 程序，并且研究了一套类型规则，作为对进程的运行时错误检查及w e b 月h 务组合相容性分析的基础。( 1 ) 关于用p i 演算建模w e b 服务组合p i 演算具有与一般程序语言类似的语法符号描述，使用了结构操作语义来表达语义，容易将抽象p i 演算映射到软件实现层次，有利于w e b 服务组合语言与形式化描述的双向转换，大大简化了w e b 服务组合语言自动验证和根据错误自动标识程序片段的操作复杂性；并且p i 演算能够根据自己本身的操作算子把子系统组合成一个大的复杂系统，可根据互模拟定义证明两个系统之间的等价关系，这样使得自动检验w e b ) 报务组合语言规范的性质：活性、安全性、公平性、正确性、可达性的目标具有可行性。更重要的是p i 演算允许在进程之间传送通道名，并可引入和输出局部名，与其它形式化描述方法( 如传值c c s ) 相比，p i 演算可描述结构动态演变的系统乜5 f ；b p e l 4 w s 是一种静态的w e b 服务组合语言，它需要事先绑定服务或者服务代理，绑定的服务之间是不能通信的，w s c d l ( w s c i ) 恰好与b p e l 4 w s 不同，如图卜l 这样的通信机制，并且现在的技术也是朝着松耦合的、动态绑定的方向发展。硕士学位论文图卜1w s c i 用例上图这样的通信机制，t r a v e l e r 调用服务代理t r a v e la g e n t ，服务代理t r a v e la g e n t 绑定服务a i r l i n e ，a i r l i n e 能够直接与t r a v e l e r 通信将结果( 机票) 返回给t r a v e i e r ，也就是t r a v e la g e n t 将与r r a v e i e r 的通信方式( 通道)传递给了a i r l i n e 。这样一种通信结构的变化就无法用传值c c s 来表示了，p i 演算正好能够描述这种通信结构的变化，所以我们以p i 演算为基础来做w e b h 艮务组合语言的形式化研究，能够将b p e l 4 w s 和w s c i ( w s c d l ) 两种模型统一起来研究。而且p i 演算上的等价理论、模态逻辑验证性质、类型系统等的研究成果也相当的j = 言十田0( 2 ) 关于类型系统类型系统是一个可行的语法工具，根据程序所计算值的种类将程序词汇进行分类，从而自动检查出错误行为6 l 。类型系统的研究和从类型理论角度对程序设计语言的研究是一个充满活力的研究领域，在软件程序语言的设计、高性能编译器和安全性方面都有着重要的应用。现代软件工程广泛的使用形式化方法，确保系统按照隐式或者显式的说明方式运行。这方面出现过一些过于理论化的框架，如h o a r e 逻辑、代数说明语言、模态逻辑和指称语义等。由于这些理论实用性不强，尤其难以被程序员所接受，所以出现了一些实用的技术，如将自动检查器放到编译器、连接器或程序分析器中的技术。至今最流行、最完善的轻量级形式化方法是类型系统。w e b 服务组合的形式化建模与相容性分析我们在p i 演算上研究类型系统出于以下几个原因：1 p i 演算是传名演算，通道和非通道数据都抽象成名字不加以区分，我们想用类型区分开来，并进一步研究w e b 服务组合语言( w s c d l 就是带类型的) 及用带类型的p i 演算进行w e b 服务组合的适配性、相容性、替换性等研究。2 在实际的工程中，结构相同但名字不相同的数据结构比比皆是，而p i演算的等价理论都是基于名字完全匹配的，我们发现这非常局限，因此我们想做类型匹配的互模拟关系。3 用类型来标记进程能够在语法层次避免运行时错误，较用模态逻辑来检验进程性质更容易实现。1 3 3 研究难点和解决方案本课题在研究过程中存在的难点以及解决的方案如下：( 1 ) b p e l 4 w s 的形式化建模通道名字的取法。既要体现原本程序的活动利于从p i 演算表达式反向标记和修改程序的错误，又要防止取名带来活动间的通信并发，我们用p a r t n e r l i n k p o r t t y p e o p e r a t i o n v a r i a b l e 四个元素构成通道的名字。b p e l 4 w s 的顺序结构的建模。我们引入b p a 演算心7 1 中的顺序算子来建模 结构，定义了其语法和操作语义，避免将顺序结构用并发算子表达的复杂性和带来的状态空间爆炸问题。d p e 机制的建模。我们重新定义了一个符号，区分开了因d p e 机制而值为f a l s e 的l i n k 和因迁移条件计算出来值为f a l s e 的l i n k 。并且我们建模时进行了特别的处理以描述d p e 机制的“p i c k 或者s w i t c h中未被选择的分支的l i n k 应被赋予f a l s e 值”的程序语义。1 i n k 程序语义的建模，特别是嵌套结构中的程序语义的建模。用并发算子来建模s o u r c eli n k 和t a r g e tli n k 会违背程序原本的非并发同步的语义，并且会带来活动的阻塞。我们把l i n k 的进入条件( j o i nc o n d i t i o n ) 和迁移条件( t r a n s i t i o nc o n d i t i o n ) 分开定义，把l i n k建模成通道，用另外一个通道传递1 i n k 与迁移条件，再用1 i n k 通道传递迁移条件来解决这两个问题。出错机制的建模是一个难点。显示错误和隐式错误的不同语法定义带硕士学位论文来建模的困难，我们提出了两种建模方法供参考。( 2 ) p i 演算上类型系统的研究我们把通道细分为了三种传输能力，因此也定义了三种通道类型。因此要重新定义类型互模拟关系，并且互模拟关系上的性质和定理需要给出证明。类型互模拟和子类型关系的研究。我们定义如果两个类型是互模拟的，那么这两个类型互为子类型。给p i 演算加上类型系统之后，需要重新定义运行时错误和规约语义。( 3 ) w e b 服务组合的相容性分析如何进行w e b 服务组合的相容性检测。我们基于w e b 服务组合系统的形式化建模研究和类型系统研究的基础上，从通道传输能力和数据类型两个方面进行相容性检查。w e b 服务组合的相容性检测要做到确实可行，我们设计了一个w e b 服务组合的相容性检测算法，并给出了一个完整的实例说明其可行性。1 3 4 本文的主要贡献和创新之处为湖南省重点科技攻关项目“业务流程装配平台”的模型检验工具完成了前期的建模工作，为b p e l 4 w s 的模型检验提供了向p i 演算进程表达式的转换规则。其中对死路排除的研究、对l i n k 的建模研究、对出错处理机制的建模研究、对补偿处理机制的建模研究等对于用进程代数来形式化建模验证w e b 服务组合具有很大的参考价值。并且在第六章我们首次涉及了用a m b ie n t 演算来建模s c o p e 机制，这对于用形式化方法深入细致的研究b p e l 4 w s 性质有很大的帮助。我们对p i 演算上类型系统进行了研究，给出了新的类型上下文环境的定义，把互模拟关系扩充到了通道类型上并且给出了相关性质和定理的证明，给出了互模拟和子类型的关系，提出了新的通信规则，为分析w e b服务组合的相容性及后续研究提供了理论依据。当然，b p e l 4 w s 的形式化建模和类型系统的研究不仅仅是为了b e p l 4 w s 相容性的检测，它们更是w e b 服务组合形式化验证的一个理论基础，比如说用于w s c d l 的形式化分析。我们提出了一种基于p i 演算和类型理论的w e b 服务组合相容性检测的方法，并给出了检测算法。这是目前首次基于p i 演算用类型系统来研究w e bw e b 服务组合的形式化建模与相容性分析服务组合的相容性，它不是停留在架构层面上，直接针对程序的运行代码，而且不需要做测试，相较于其他的分析方法更具有可行性。该方法如果验证了w e b 服务是相容的同时也说明了该w e b 服务组合流程的行为是正确的、也没有死锁，也可以用于w e b 服务发现、w e b 服务替换等w e b服务组合的研究，而且很容易将这种方法移植到对w s c d l ( w s c i ) 的分析上。这也是本文最大的创新点。1 4 论文的组织论文余下的章节对课题研究的内容进行了详细的阐述。第二章是b p e l 4 w s 规范和p i 演算的语法和操作语义的介绍，在这一章的最后我们定义了扩充的顺序算子的语法和操作语义。第三章是对b p e l 4 w s 语言详细建模工作的研究。仔细研究了通道取名的方法、d p e 机制的建模、l i n k 的建模、原子活动的建模、结构化活动的建模、e报警机制的建模、出错和补偿机制的建模、s c o p e 的建模等，最后给出了一个旅游预订服务的完整建模实例。第四章是p i 演算上类型系统的研究。首先我们介绍了多元p i 演算的规约语义，用单元p i 演算编码多元p i 演算带来的运行时错误，从而引出了p i 演算上的类型系统的定义；接着介绍了类型互模拟关系及其以上的一些性质和定理并给出了他们的证明；在探讨了子类型关系后给出了进程类型定义良好( w e l l t y p e d ) 的规则，最后重新定义了进程的通信规则。第五章在前两章研究的基础上进行w e b 艮务组合相容性的分析。第一节和第二节对w e b 服务组合相容性进行了讨论，给出了相容性的几个等价定义以及相容性的p i 演算表达；给出了w e b 服务组合相容性检测的算法；第三节给出t b p e l 4 w s 程序s n w e b j 报务的类型化p i 演算的建模方法以及进程上下文的确定方法；本章最后给出了一个完整的实例及反例说明了我们的检测算法的可行性。第六章我们尝试了用a m b i e n t 演算来建模b p e l 4 w s 的s c o p e ，将s c o p e 来建模成环境，用a m b i e n t 演算的出、进、打开环境来建模出错机制的向父级s c o p e抛出错误的高级属性。第七章总结了本文的工作，并对今后的工作提出了展望。硕士学位论文第二章b p e l 4 w s 规范和p i 演算理论这一章介绍w e b 服务组合语言b p e l 4 w s 规范和进程代数p i 演算的基本理论，在最后一节给出了我们扩充的顺序算子的语法和语义，奠定后续研究工作的理论基础。2 1b p e l 4 w s 语言业务流程执行语言b p e l 4 w s ( b u si n e s sp r o c e s se x e c u ti o nl a n g u a g ef o rw e bs e r v i c e s ) 是专为整合w e b 服务而制定的一项规范标准，是i b m 的w s f l和m i c r o s o f t 的x l a n g 的结合物，目前已经成为业界标准h 3 。w s f l 支持图形化的流程，而x l a n 6 在结构化构造方面有独到的方法，b p e l 4 w s 正是吸取了两者的优点，同时摒弃了一些复杂繁琐的部分，形成了一种较为自然的描述业务活动的抽象高级语言，能够定义企业内部、企业间基于w e b 服务的业务流程( 如订货业务、业务提示、处理客户提出的问题等) 如何相互协助。b p e l 4 w s 的文法是完全基于x m l 规范的，它支持实现可执行的业务流程。作为可执行流程的实现语言，b p e l 4 w s 将一组现有的服务整合起来，从而定义一个新的w e b 服务，因此，b p e l 4 w s 是一种实现w e b 服务整合的语言。与其它任何w e b 服务一样，整合的服务能够被其他的服务或者客户端访问，整合服务的接口被描述为w s d lp o r t t y p e 的集合，流程整合指明了服务接口与整合的总体执行的配合情况。图2 - 1 是b p e l 4 w s 流程实现的w e b 服务的视图。i n m l yo p e r a t i o ni n p 呐n l yo 盼a t i o n图2 一lb p e l 4 w s 流程实现的w e b 服务的视图b p e l 4 w s 流程本身基本上就是一个流程图，类似于用来表达算法的流程图。b p e l 4 w s 中存在一些基本活动：调用某个w e b 服务的操作( ( i n v o k e ) ，w e b 服务组合的形式化建模与相容性分析等待一条消息一来响应由某人从外部进行调用的服务接口的操作( ) ，输出( 回应) 操作的响应( ) ，等待一段时间( ) ，把数据从一个变量复制到另一个变量( ) ，抛出错误的操作( ) ，终止整个服务实例( ) ，或者什么也不做( )盘占寸0b p e l 4 w s 支持结构化活动，也允许递归地组合结构化活动。结构化语句主要有：定义一组动作顺序执行的序列( ) ；使用现在常见的“c a s e - s t a t e m e n t 办法来产生分支( ) ；定义一个循环( ) ；执行几条可选路径中的一条( ) ；以及指明一组步骤应该并行地执行( ) 在并行地执行的一组活动中，可以通过使用“链接 ( 1i n k ) 来指明执行顺序方面的约束，l i n k 是数据流的控制。b p e l 4 w s 把与流程交互的其他服务称“伙伴”( p a r t n e r ) ，“伙伴 可以是流程将其作为一个组成过程进行调用的服务( 被调用的伙伴) ，也可以是那些调用该流程的服务( 客户机伙伴) 。另外，b p e l 4 w s 还引入了一种表示第三方声明的机制：服务链接类型。通过它我们可以说明了两个服务之间的关系。服务链接类型定义了一组角色，其中每个角色指明一组p o r t t y p e ，当两个服务彼此交互时，服务链接类型就是对这个服务如何交互一一各方本质上提供了什么样的声明。b p e l 4 w s 对于错误的捕获和处理也有相应的机制，b p e l 4 w s 通过和 构造来处理错误( 故障) ，或者通过 来处理显示或隐式的故障。此外，b p e l 4 w s 支持“补偿”这个概念，它是一种允许流程设计者为某些不可逆的动作实现一些补偿动作的技术，比如说一些操作取消等等。2 2p i 演算p i 演算具有两个基本的实体，名字和进程。名字即为连接的名字，进程通过他们共享的名字进行交互，而关键的要点在于进程在交互中通信的数据同样是名字，交互中接受的名字能够用来参与其他交互通过接受名字，进程能够动态得到与其他进程进行交互的能力。因此，整个系统的结构，即系统构件之间的连接关系能够伴随时间演化。硕士学位论文2 2 1p i 演算的基本语法我们对w e b 服务组合语言用多元p i 演算来建模的。多元p i 演算的基本语法定义如下啪m 引：p ：= mi plpl 谚pl ! 尸m ：= 0l 刀pl m + m石：= 孑 l x ( 三) l rl x = y 万p i 演算中最简单的实体是名字，进程通过名字进行交互，并在交互当中传递名字。上述p i 演算的语法定义中，x 是单个名字，芽与z 互为对偶名字( c o - n a m e s ) ，进程通过对偶名字进行交互。y 。，三是多个名字组成的元组。p是p i 演算中实体进程的语法定义，m 是p i 演算中“和 ( s u m m a t i o n s ) 的语法定义，用以表达选择执行关系。p i 演算的语法给出进程能够执行的四种动作( a c t i o n ) ，称为前缀( p r e f i x e s ) 。进程通过执行这些基本动作而进行演化。p i 演算的语法的解释如下：( 1 ) 0 表示非活动的进程，即不做任何动作的进程。在有些模型检测工具中，0 也表示死锁，在我们的研究过程中认为有必要把死锁和进程正常演化到达的0 进程分开。( 2 ) 前缀万p 表示具有万表示的行为能力，该能力执行后接着执行进程p ，顺序执行。输出前缀i 尸表示通过名字i ( 通道x ，通道在用作输出时在通道名字上面加一横) 输出名字元组夕，然后执行进程p 。如果输出单个名字y ，而非名字元组，则省略括号，记为_ y p 。输入前缀x ( 三) p 表示通过名字x 输入名字元组，并用输入的名字元组替换进程p 中的三，然后执行替换后的进程p 。三也称为占位符，如通过x 输入接受的名字元组是歹，那么替换结果就为尸 歹三) 。内部动作前缀f p 表示执行对外不可见的内部动作彳后执行进程尸。匹配前缀 z = j ，k p 表示如果z ，y 是同一名字，则执行进程万p ，否则成为0 进程。( 3 ) “和 m + 鸠表示选择执行m 。，鸠两个进程中的一个。只要表达式中一个分支被选择执行那么另外分支的行为就变为0 。( 4 ) 并发p lq 表示两个进程p ，q 并发执行。p 和q 能够独立并发执行并能够w e b 服务组合的形式化建模与相容性分析通过共享的对偶名字进行通信。( 5 ) 限制凹表示元组三中的名字是进程p 的局部名字，p 不能通过其中的名字与其他的进程交互，但在进程p 的内部能够使用这些名字进行通信。在4 1 2 节，我们将介绍结构同余规则，通过结构同余规则可以将受限域进行扩展。对于v 凹的另外一种描述是产生一组新的名字，这些新产生的名字不能与进程p 中的名字同名，新的名字可以通过其他不受限的名字向外输出。( 6 ) 复制! p 表示无限多个进程p 并发执行，! p = p lp | 。2 2 2p i 演算的迁移语义p i 演算的迁移语义通过定义进程能够执行的动作( a c t i o n ) ，表明进程的行为能力，能够描述系统内部活动，也能描述系统与环境的交互活动。p i演算中，定义迁移语义时，它的标记动作分为四类，这四类标记动作与进程语法定义中进程的前缀相似，但并不完全相同，定义如下：a ：= 五yl 砂lx ( z ) if动作的集合定义为a c t 。第一类动作砂称为自由输出( f r e eo u t p u t ) ，表示通过名字x 发送名字y ；第二类动作x y 称为输入( i n p u t ) ，表示通过名字x 接受名字y ；第三类动作；( z ) 称为限制输出( b o u n do u t p u t ) 表示通过名字x 发送一个新的名字( f r e s hn a m e ) ，新名字是进程交互中生成局部私有名字并发送该名字，z 是占位符，代表该新名字；第四个动作f 表示进程内部动作。p i 演算的迁移语义定义如下：o u t 对p 山尸刚uf p 二一p，p 山p s u m 也二二二_ 一p + q _ p p 马p p 马pc o m m l 二_ 二二羔o 二芝尸 g 二哼尸 q 髓s 嵩( a )v z p 三专坦p 、p 山尸i 也p a c t _ 二= 一i n px ( z ) 。p 生专e y z m a t 至：! 主! ! ：【x = x 】万p 三专尸p a r - l 揣b n ( a ) n f n ( q ) = 矽pp 三一p lp。c l o s e - l 蒜兰斋并z 咧q ，pp 与v z ( p ip t )、。7o p e n ! 三呈! z x硕士学位论文r e p c o m m ! 三竺! ! ! 三竺!，! j p - ( p i 尸”) l ! pr e p c l o s e 里兰兰! ! ! 三兰竺z 萑姗11 j p 与( 坦( p l 尸”) ) j ! 尸图2 - 2p i 演算的迁移语义在上图表示的迁移语义中，b n ( g ) 表示动作口的受限名字，f n ( q ) 表示进程q 的自由名字，”位) 表示动作口中的名字。o u t 砂p 玛尸表示进程砂尸能够通过通道x 输出一个名字y 演化成进程p ；i n