（计算机软件与理论专业论文）web服务组合建模和验证技术研究.pdfVIP

东南大学学位论文独创性声明 m l l l l l l l 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 f i i l | i i l y 1 7 5 4 6 7 1 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成 果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得东南大学或其他教育机构的学位或证书而使用过的材 料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了 谢意。 研究生签名： 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复 印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和 纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布 ( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。 研究生签名： 酶师签名： 摘要 摘要 面向服务的体系结构( s e r v i c e - 0 晡e n t i 耐a r c h 慨c t u r e ，s o a ) 是分布式计算和软件开发的最新发展方 向。s o a 的目的是以w 曲服务为基础，有效地解决在分布、动态、异构环境下分布式应用集成问题。 w 曲服务作为一种自治的、与平台无关的网络化构件，具有松耦合、支持动态组合和重配置等特点， 从而为i n t e m e t 环境中软件开发和分布式应用提供了新的技术。 通常，将多个服务动态地组合成一个新的组合服务以满足用户的需求。描述这种组合过程的w | e b 服务组合描述语言主要是w s b p e u w 曲s e n r i b u s i n e s sp r o c e 豁e x e c 嘶l 锄g 嗯g e ) 和w s d i w 曲 s e n ，i c e sc h o r e o 辨埘1 yd e s c r i 硼o nl 锄g u a g e ) ，这些语言存在两个方面的缺陷：一是，由于这些语言都是 基于) ( i 咀，的，缺乏建模的理论基础；二是，这些语言未能提供验证其规约正确性的方法。 考虑以上问题，不仅要保证在设计阶段w 曲服务组合规约的正确性，还要保证在运行时阶段w 曲 服务组合规约的正确性，所以本文系统地研究了w 曲服务组合建模、静态验证和动态验证三个方面， 主要研究成果如下： ( 1 ) 研究了w 曲服务组合建模的问题，提出了一种基于i 沮，模型的w 曲服务编舞语言w s c d l 建模方法。采用沮。构件图表示w s c d l 的结构模型，用u 咀，顺序图来建立w s c d l 中各个角色 之间的活动模型，并自动地从顺序图中生成i m ，状态机图模型来表示单个角色的行为模型，并从w s d l 规约中获得w s c d l 的数据流信息，用u l 沮。类图来表示数据流。该方法提供了图形化的前端，方便 了设计者直接建立服务组合模型，并考虑w 曲服务组合过程中数据流的建模问题。 ( 2 ) 研究了w 曲服务组合的静态验证问题，提出了一种基于皿模型的w s - c d l 的模型检验方法。 该方法将切帆模型表示的w s c d l 转化为c a d e n c es m v 模型检验工具的输入，并验证系统模型是否 满足规定的属性。该方法不仅能够验证w 曲服务组合过程中的结构属性和行为属性，而且能够验证数 据属性。实验结果表明，该方法能够验证中等规模的带数据的w 曲服务组合中的关键属性。 ( 3 ) 研究了运行时w 曲服务组合过程中时态属性的动态验证问题，提出了一种基于p s c 的w 曲服 务组合过程中时态属性的监控方法。引入了属性序列图( p 删s e q u 钮c ec h a n p s c ) ，定义了p s c 的 形式语法和语义，采用运行时监控技术来持续地监控w 曲服务组合过程的执行轨迹是否满足p s c 表示 的时态属性。实验结果表明，该方法能够有效地检测运行时w 曲服务组合过程中存在的时态错误。另 外，由于p s c 图形化的优点，使得表示时态属性简单、易于理解，从而解决时态逻辑表示时态属性复 杂和不够直观的问题。 “) 研究了运行时w 曲服务组合过程中时间属性的动态验证问题，提出了一种基于耵s c 的w 曲 服务组合过程中时间属性的监控方法。鉴于p s c 图形化的优点，将p s c 扩展为t p s c ( 瓢m e dp s c ) 来表 示时间属性，给出了基于时间b n c l l i 自动机的1 1 p s c 操作语义，并用实时规约模式来评估t p s c 的表达 力。采用运行时监控技术检测w 曲服务组合过程的执行轨迹是否满足1 1 p s c 表示的时间属性，并采用 基于假设检验的统计技术对这些时间属性在运行时成立的概率进行计算。实验结果表明，该方法能够在 运行时精确地监控时间属性成立的概率，并具有良好的性能。 ( 5 ) 设计和实现了两个原型工具t - w s c d l 和w s p s cm o l l i t o r ，以支持以上提出的理论和方法。 t w s c d l 实现了基于u 咀，的w s c d l 建模方法和静态验证方法。w s - p s cm o l l i t o r 实现了基于p s c 的时态属性监控方法和基于t p s c 的时间属性监控方法。 关键词：w 如服务、w 曲服务组合、统一建模语言、属性序列图、模型检验、运行时监控 东南大学博士学位论文 a b s t r a c t s o a ( s e n r i c e - ( ) 一e n t e da r c h j t e c t u 陀) i st 1 1 em o s tp r o m i s i n g 缸训o fd i s t r i b u 湖c o m p u t i l l g 锄ds o m v a 他 d e v e l o p m e n ln eg o a lo fs o ai st 0e 伍c i e n t l ys o l v em ed i 矧b u t e d 印p l i 洲o nh e 鲥i o nb 丛e d w e b i c 骼 i i l d i s t r i b i l t e d ，d y n 锄i c锄dh e t e r 0 毋m e o u sa l v i r o m n e n 协w e br “c e sa 他a u t o n o m o u s p l a t f 0 加- i i l d e p e n d e n tn e 佃o d ( c o m p o n e n t st i l a lh a v es o m en e w 砌b u t e ss 眦h 弱1 0 0 辩c o u p l i l l g ，d ) r i l a m i c c o m p o s i 廿0 1 1 ，r e c o m i 舭t i o i l p r o v i d i n gan e wt e c l l l l i q u ef 研d i s n 伯删a p p l i c 鲥o n 柚ds o f t w a 陀d e v e l o p m e n t 0 ni m e m e t s o m es e n ，i c e s a 他d y i l 锄i c a l l yc o m p o s e dt of 0 m an e wc o m p o s i 钯s e n r i c ef o r s a l i s f y i i l gu r s 帕q u i 崩n e 吣n ec o r n p o s i t i o np 眦e s si sd e s 嘶b e db yw 曲s e r v i c ec o m p o s i d o nd e s c r i p t i l 锄g u a g e ss u c h 勰 w s b p e l ( w 曲s e r v i c eb 璐i i l e s sp r o c e s se x e c 面0 nl a l l g 岫g e ) 锄dw s - c d l ( w 曲s e i c 懿c h o f e 0 - 印l p h y d e s c r i p t i o nl m g 阻g e ) h o w e v e r ，廿l e s el 锄舒m g e sh a v et 、m a i l lp r o b l 锄s o n l eo n el l a i l 也也e l 觚g u a g 鹤 a 他b 勰e d x m l ，锄dl a c kt h et l l e o 础c a lf o u n d a t i o no fm o d e l i l 培o nt t l eo t 量l e rl l a l l d ，吐l e l 锄目l a g e s m o t p r o v i d e 锄ym e a i 岱t 0v 耐黟廿l ec o 叮e c n l e s so fs p 吧c i 6 c 鲥0 n h lo r d e rt 0s o l v e l e p r o b l e m s ，廿l ed i s r t a t i o ns y s t e m a 士i c a l l yi i i v e s t i g a t e s 廿i em o d e l i n 舀嘶| t i ca n d d ) r l 姗i cv e r i f i c a t i o no fw b bs e n ，i c ec o m p o s i t i o n n 0 to i l l yn l ec o r 陀c 缸l e s so fs p e c i f i c a 矗n e e d st 0b ev e r i f i e d a fd e s i 秒t i m e ，b u ta l d 脚i cv e f i c a t i o nt e c h n i q u ei su s e df o rn l e 笛s u r 锄c eo fc o r r e c n l e s so fs p e c i f i c 撕o n a tm m i m e t h e r e f o 他，t l l em 咖c 州b u t i 0 i 毽o fm ed i s s e r t a t i o na 他l i 曲e d 私f o l l o w s ： f i r s t w ep r o p 0 辩am o d e l i n ga p p r o ho fw s c d lb 雒e do n 切儿m o d e l s w 色u u v 几c o m p o n e n t d i a g m st 0r e p 陀s e n t 也es 仃u 曲l r a lm o d e io fw s d l a 嘶v 时m o d e l 锄o n ge hr o l ei i lw s c d li s m o d e l e db ym 他s e q u e n c ed i a 鲈姗s ，廿l 跚l 玎沮，吼| l em a c l l i n em o d e l sr e p 陀s e r n i n gb e l l a ：v i o rm o d e lo fs i n g l e r o l e a 坞钒i t o m a t i c a l l y 誉m e r 纳e d1 j r o mu m ls e q u e n d i a g 阳m s d a t a n o wi s0 l ，t a i l l e d 五吣mw s d l s p e c 泊c a l i o n 锄dt l l 朗i sp r e n t 酣b yu m lc l 鹬sd i a g 舢s 1 1 1 ea p p r o a c hp r o v i d e sa 可a p m c a l 锄t 蜘df o r d e s i 印e 搭t 0 曲e c yd e s i 印w 曲辨r v i c ec o m p o s i t i o nm o d e l 1 1 1 ed a 协n o wi i lw e bs e n ，溉c o n l i ，0 s i t i p l d c e s si sa l s 0c o r 塔i d e r e d s e c o n d ，w ep r o p o s eam o d e lc h e c k i n g 印p r o a c ho fw s c d lb a do nim m o d e la ld e s i 印- t i m e 1 k u m lm o d e l sa 陀t r a i l s l a t l 觅i l l t 0t l 他i n p u tl 锄g u a g eo fc a d e n c es m vm o d e lc h e c k e r 矗”v 嘶f y i n gw h e m e r u l jm o d e l ss a l i s 黟d 豁i r e dp r o p c 桶e s t 1 l e 雒l p l 抛c h 锄n o to n l yc 觚州黟s 仃u c t u 随l 锄d 坟妇l v i o f a l p r o p e f t i e s ，b u ta l s oc 锄v 耐f yd a ：t ap r o p e n 慨i 1 1w s d l 1 e x p e 向e n t ss h o w 吐圮a p p r 0 h 啪v 嘶匆 s o m ec r i t i c a lp r o p e n i e si i lam i d d l e s c a j ed a 删c h e dw 曲鲫i c ec o m p o s i t i o n 1 f l l i l 吐、ep r o p 0 锄a p p r 0 hf 0 rm o m t o r i n go f t e m p o r a jp r o p e n i e si i lc 0 i r l p o s 确s e r v i c eb 豳e do np s c 砸 r 眦m m e an 0 、，e ls n 撕伊b a s e dn o t a t i o np s c ( i 咖r 哆s e q u e n c ec h a r t ) i si n 仃o d u c e d t h ef o n n a ls y n t a x 锄d m 觚t i c so fp s ca 他d e f i n e d w b 廿l e nu n m t i m em o i l i t o r i i l gt l m i q u et 0c o n t i m l o u s l yd e t e c t 、v h e 吐l e rt h e e x e c l n i 昀c 0 fw e b 鲫r v i c ec o m p o s i t i o n 勰c 0 璐i s t e n tw i m t e m p o r a lp r l 耻i t i e ss p e c i f i e db yp s c 1 k 叩血n e 力峪s h o w l a l 也e 印p hc a ne 伍c i e m l yd 酏t 廿l ee r r 0 硌i i lc o m p o s i t e n r i c ea ln m t i m e m o r e o v e r t e m p o r a lp r o p e r t i e sr 印他s e i i t e db yp s ca 托s i m p l e 锄de 丛i l yu n d e 倒 0 0 d 、：i l i c ha d d r e s sn l ep r o b l e mn l a t p r o p e n i 鹤他p r e n t e db yt e m p o r a ll o 西c sa 豫n o tm i t i v ea n dc l e 托 f o r 电w ep p o 锄印p hf o rm o l l i t o r i i l go ft i m 酣p r o p e f t i e si i lc o m p o s i t e 靶n ，i c eb 舔e do n1 1 p s c 砒 n l 而m e c o i l s i d e r i l l gn l e 卿l l i c a la t t r i b u t eo fp s c ，p s ci s 咖d e di n t ot p s c ( 1 r i m c dp s c ) t 0 陀p r e 湖t t i m e dp r o p e n i 骼t h e 靶m 枷c so ft p s ci s 舀v b a s e do n 缸m c db u c l l ia u t o m a l o i l 锄dn l ec x p r 鹳s i v 明豁so f t p s ci sm e 笛删b a s e do n 删咖es p e c i 6 c 砒i o np a t t e n lw bn l e nu 辩n m t i m em o i l i t o r i n gt e c 蜥q u et 0 c o n t i l l u o 啪l yd e t e c tw h e t h e r 吐l e t u a lb e h a 啊o ro fw e b 辩州c ec o m p o s i t i 彻p 撇s ss a 舡s f i 懿妇：钦p e c t e d t i m 酣p r o p c n i 骼t h ea p p 瑚c hc a i la l c 伽叽tw h 甜1 e i l ep m b a b i l 时f b rat i m e dp r o 哼t yh o l d sa l 邝n 吐m e t h e 鼬e w o 呔h 雒b 啪a p p l i e dt oac a s n j d y 锄das 鲥髂o f e x p e 柚e 鹏h a v eb n 陀p c 帆e d ，吐l 砒v a i i d a l e 血ep e r f b 咖柚o f t i i ep r o p c ，s e d 纳m e w o 嗽 捅要 f i i l a l l y t 、) i r op r o t i 啊p et o o l sc a l l e dt - w s - c d l 锄dw s p s cm o m t o ra r ed e s i g i l e d 觚di m p l e m e i l t e dt 0 s u p p o r to u r 印p r o a c h 鹤t - w s d lc a l lb eu s e dt 0m o d e l 锄d 涨i c a l l yv 耐匆t l 怆w s - c d ls p e c i f i c 胡o m w i l i l ew s p s cm o 砷0 rc 觚b e 璐e dt 0m o d e l 觚dm o i l i t o rt e m p o r a l 锄dt i m e dp r o p e n i e si nc o m p o s i t e 鲫r v i a l 九m t i m e 鼬y o r d s ：w e bs e i ，w e bs e r v i c ec o m p o s i t i o i l u i l i f i e dm o d e l i n g1 觚g u l a g e ，p r o p e n ys e q 鹏n c ec h 矾 m o d e lc h e c k i n 吕m n t i m em o l l i t o r i l l g 东南大学博士学位论文 目录 摘要i a b s 时a c t i i 第一章绪论1 1 1 研究背景1 1 1 1 面向服务的计算和面向服务的体系结构1 1 1 2w b b 服务2 1 1 - 3w e b 服务组合2 1 2 研究动机和研究意义3 1 2 1w 曲服务组合建模。3 1 2 2w 曲服务组合的静态验证3 1 2 3w 曲服务组合的动态验证3 1 3 研究内容和主要贡献4 1 4 文章结构5 第二章研究基础与现状7 2 1w 曲服务组合建模。7 2 2w 曲服务组合的静态验证7 2 2 1 基于自动机的方式。7 2 2 2 基于进程代数的方式一8 2 2 3 基于p e t r i 网的方式8 2 2 4 典型的w 曲服务组合静态验证方法比较8 2 3w 曲服务组合的动态验证9 2 3 1s l a 监控。l l 2 3 2 智能监控、动态监控和健壮性监控1 l 2 3 3 需求监控、交互监控和诊断监控1 2 2 3 4 规划监控和自动监控1 2 2 3 5 选择监控和p l a s t i c 1 2 2 3 6c r e m o n a 和c o l o m b o 1 3 2 3 7 典型的w 曲服务组合监控方法比较1 4 2 4 本章小结1 4 第三章基于u 札模型的w e b 服务组合建模15 3 1w s d l 和w s d l 简介1 5 3 1 1w s d l l5 3 1 2w s d l 1 5 3 1 3 实例研究1 6 3 2 基于u l 儿模型的w s c d l 建模1 7 3 2 1 构件图l8 3 2 2j 顿序图。1 9 3 2 3 状态机图2 l 3 2 4 类图2 5 3 3 本章小结2 7 第四章基于u 札模型的b 服务组合静态验证2 8 4 1 模型检验2 8 4 2c a d e n c es m v 模型检验工具2 8 4 2 1s m v 语言2 9 目录 4 2 2s m v 属性规约。3 0 4 2 3 验证方法31 4 3 带数据的状态机图转化为s m v 语言3 1 4 3 1 模型转化过程3l 4 3 2s m v 代码生成步骤3 2 4 3 4 验证过程。3 3 4 4 实验分析。3 4 4 4 1 属性表示3 4 4 4 2 实验结果3 5 4 5 本章小结3 8 第五章基于p s c 的w e b 服务组合中时态属性的动态验证3 9 5 1w s b p e l 3 9 5 2p s c 3 9 5 2 1p s c 简介4 0 5 2 2p s c 形式语法4l 5 2 3p s c 形式语义4 2 5 3 一种基于p s c 的时态属性监控方法4 9 5 3 1 基于a o p 扩展b p e l 引擎。5 0 5 3 2 属性表示5 l 5 3 3 观察器和分析器5 4 5 3 4 实验分析。5 6 5 4 本章小结5 7 第六章基于t p s c 的w 曲服务组合中时间属性的动态验证5 8 6 1t p s c 。5 8 6 1 1 时间扩展5 8 6 1 2 基于时间自动机的语义5 9 6 1 3t p s c 的表达力。6 3 6 2 一种基于t p s c 的w 曲服务组合过程中时间属性的监控方法6 5 6 2 1 基于a o p 扩展b p e l 引擎6 6 6 2 2 属性表示6 7 6 2 3 观察器和分析器6 9 6 2 4 实验分析7 2 6 3 本章小结7 4 第七章b 服务组合建模和验证原型工具7 5 7 1w 曲服务组合建模和静态验证原型工具7 5 7 1 1 基本框架7 5 7 1 2 工具实现7 5 7 2w e 服务组合动态验证原型工具7 7 7 2 1 基本框架7 7 7 2 2 工具实现7 8 7 3 本章小结。7 9 第八章总结与展望8 0 8 1 论文主要工作总结8 0 8 2 后续工作展望8 0 v 第一章绪论 第一章绪论 面向服务的计算( s e n r i c e o r i e n t e dc o m p u t i n g ，s o c ) 和面向服务的体系结构( s e n ，i c e 旬r i e n 白e d a r c h i t e c t u r e ，s o a ) 是软件开发技术进步和分布式系统发展的一个新的里程碑。服务作为一种自治、开 放和平台无关的网络化构件，使得软件开发技术和分布式应用具有更好的复用性。 1 1 研究背景 纵观软件技术发展的历史，即从起初的个人作坊、面向过程的结构化方法、面向对象的开发方法到 面向构件的开发方法，这些开发方法无不对软件技术的发展产生了深远的影响。在个人作坊阶段，程序 设计仅是一种发挥创造才能的活动，程序往往被称为只是少数人编写的“艺术品”。而面向过程的结构 化方法，即强调数据结构、程序模块化结构等特征，从而大大提高了程序的可读性。伴随着结构化软件 技术而出现的软件工程方法( 包括c a s e 工具) ，使得软件开发的工作范围从只考虑程序的编写扩展到整 个软件生命周期( 包括需求分析、设计、实现、验证和确认、运行和维护) 。从而，软件由个人作坊的“艺 术品”变为团队的工程商品。而面向对象的方法( 0 叼e 删明由e d ，o o ) 很大程度上提高了软件的易读性、 可维护性、可重用性，进一步使得从软件分析到软件设计的转变非常自然，因此大大降低了软件开发的 成本。另外，通过有效地重用o o 技术开辟了提高软件生产率的新篇章。之后，面向构件技术的出现实 现了软件产业向工业化生产的飞跃，带来了新的契机。同样，由于网络和分布式应用的广泛发展和应用， 面向服务的计算( s o c ) 和面向服务的体系架构( s o a ) 的应运而生，是对传统的软件开发技术的改进，势 必会对软件技术发展历程产生深远的影响。 1 1 1 面向服务的计算和面向服务的体系结构 随着网络和分布式计算的快速发展，现代企业的软件开发面临的挑战是快速改变的市场条件、企业 外部环境的不断变化，企业内部的结构不断调整等。现代企业只有快速地适应这些多变的需求，才能紧 跟时代的步伐，在激烈的市场竞争环境中立于不败之地。所以传统的“一次性”软件开发方式显然不能 满足这种快速增长和多变的需求。而如何解决企业应用所面临的挑战是当今软件界的焦点问题之一。 s o c 和s o a 的提出为解决这一难题提供了新型的计算模式和软件开发方法。 s o c 以服务为基础来支持快速、低成本地开发可组合的分布式应用【l j ，其中，服务是自治的、平台 独立的计算实体。服务可以完成基本的功能，也可以通过组合已有的服务来完成复杂的功能。通过描述、 发布、发现和动态地组合服务从而形成规模更大的系统，该系统具有分布式、互操作性、重用性、可扩 展性和动态演化速度快等特剧2 1 。根据服务的思想，软件系统中任何代码或任何构件都能够被重复使用， 并封装为网络上可使用的服务。这体现了“面向服务”的编程方法的核心思想，即通过发现和调用网络 上已有的服务来组合新应用而不是通过自己编写新的程序来实现这些应用i l j 一般而言，服务都以独立 于其使用的方式被开发，这使得服务提供者和请求者是以松耦合的方式连接的。 s o a 是一种基于s o c 的设计方式，在服务的生命周期( 从需求分析、设计、实现、预发布、运行以 及演化) 中，指导着服务的创建和使用的方方面面。s o a 也是一种定义和提供i t 基础设施的方式，允许 分布式应用之间交互数据、参与业务过程，而不管分布式应用是基于何种操作系统或采用了何种编程语 言【3 l 口 。 当前一些研究组织和世界著名大学都深入地研究s o c 和s o a ，研究人员不断地提出新的面向服务 的基础理论、方法和应用。针对以面向服务的计算和面向服务的软件开发为主题的国际会议 ( c o n f e r e n c e ) 、研讨会( s y m p o s i 啪) ，著名的如i c w s 、s c c 、l c s o c 、s o s e 等。同时，各大学术团体和 标准化的组织，如o a s i s 、w 3 c 也不断推出s o a 相关技术标准和规范，诸如w s d l ( w 曲s e n ，i c e d e f i l l i t i o nk g u a g e ) h 、i j l ) d i ( u i l i v e r s a ld c s c r i 嘶o i l d i s c o v e 吼锄di n _ t e 野a l i o n ) o ) 。、w s - b p e l ( w 曲s e n r i c e b u s i i l e s sp 砌鄢se x e c 佣o n 踟g u a g e ) 口、w s d l ( w 曲s e n ，i c ec h o 删溜即h yd e s c r i p t i l a n g 岫g e ) 州、 s l a ( s e n ，i c el e v e la g r e e m t ) p j 、w s - p o l i c 矿、w s a 舢e 耐1 等。 在工业界，w 曲服务技术也逐渐成为当前s o a 实现的主流方式，包括m m 、微软、b e a 等在内的 全球知名企业和各大研究机构都在通力合作，促进w 曲服务技术的发展和成熟。美国著名i t 咨询公司 1 东南大学博士学位论文 g a m l e r 把s o a 选为2 0 0 6 年1 0 大战略技术之一，并预测到今年底将有6 0 的企业会采用s o a 作为其 基本的体系结构【1 2 】。 总之，s o c 和s o a 是软件技术发展的新的里程碑，是继面向对象和面向构件的编程思想以来一种 变革性的软件开发技术。实践证明，s o c 和s o a 对软件的技术的发展以及企业的i t 架构将带来巨大 的影响。 1 1 2w e b 服务 w 曲服务是s o a 的一种具体的实现，或者说是二种具体的应用。关于w 曲服务的定义，当前有很 多版本，本文给出w 3 c 对w 曲服务的定义，即“w r e b 服务是由嘲标识的软件应用，可以用x l 儿来 定义和描述其接口和绑定，并且可以被发现，通过基于i n t e m e t 的协议以帆消息交换的方式与其他 软件直接进行交互【13 1 。” 服务编舞( v 幅七d l ) 服务编捧( b p e l ，b p m l ) 发布和发现( u d d i ) 服务描述( w s d l ) 消息扩展 ( w s - a d d 伦豁i n g ，w 孓 r e i j a b i e m e s g i n g 、，v s p o i i c y v 姻- s e c u 啊。w s 七一i n a a o n w s - t 亿n s a b o n ) 消息( s o a p ) 传输协议 ( h 1 t p ，s m t p ，0 r b ，o p ， j m s ) 图l lw e b 服务相关基本技术 有关w 曲服务的技术体系，其中核心技术是：s q a p 、w s d l 和i j l ) d i 。w 曲服务相关技术如图1 1 所示，其中最底层的传输协议是i i l t e m e t 或其他分布式计算平台广泛使用的标准，这表明w 曲服务技术 可以架构在多个分布式平台之上，其他规范是在传输协议的基础上扩展而来的。w 曲服务之间的通信 是通过互相传递符合s o a p 协议的x m l 消息实现的。消息扩展规范的主要作用是提供服务实例寻址以 及在消息级别提供可靠、安全、业务等质量保障。w s d l 是用来描述服务接口的，u d d i 提供了服务发 布和发现的服务注册中心规范，服务编排( o r c h e s 仃a l i o n ) 和编舞( c h o r e o 伊a p h y ) 是w 曲服务组合过程的描 述语言。 1 1 3w e b 服务组合 w 曲服务组合是指“通过组合基本w 曲服务从而提供增值服务的能力，这些基本服务可能由别的 组织提供的”。该定义的含义是：( 1 ) 服务组合需要使用其他服务；( 2 ) 组合以后形成的服务具有新的功能； ( 3 ) 服务组合使用的基本服务可以是组织外部的。已提出很多服务组合语言，比如池a n g 【1 4 j 、w s f l 【1 5 】、 b p m l 【1 6 l 、w s c i 【17 1 、w s c l 【1 引、o w l s 等。当前主流的服务组合语言有w s b p e l ( b p e l 4 w s ) 、w s d l 和o 、i s 三种语言。w s b p e l 是服务编排描述语言中代表。服务编排是指描述服务组合的一个过程， 从服务组合的某个参与者的角度来描述参与组合过程的服务之间的消息交互，从而完成组合服务的应用 逻辑【2 0 1 。w s d l 是服务编舞建模语言中代表。服务编舞从各个参与者对等的角度，描述参与某次协 作中多个服务之间的对等消息交互协议。o w l s 是以基于语义的方式通过共享本体实现w 的服务之间 的自动发现、组合。o w l - s 提供了描述w 曲服务的词汇表，不但可以描述服务的语义，而且能够进行 适当的推理，使得w r e b 服务具有机器可理解性和易用性，从而具有自动发现、组合、调用、互操作和 监控的能力。 2 第一章绪论 1 2 研究动机和研究意义 当前w 曲服务组合描述语言存在两个主要问题：其一，这些语言都是基于沮，的，缺乏建模的理 论基础，因此这些语言的建模理论值得进一步深入的研究。其二，由于这些语言本身并不能提供完善的 机制保证其规约的正确性，故如何保证这些语言描述的服务组合的正确性也是另一个值得研究的问题。 与传统的软件不同的是，w 曲服务组合具有高动态性的特点，在运行时可能由于用户需求或环境 发生改变，而导致组合服务发生改变。所以，需要从运行前和运行时两个阶段来验证服务组合建模的正 确性。为了解决以上问题，下面从w 曲服务组合建模、w 曲服务组合静态验证和w 曲服务组合运行时 动态验证三个方面阐述研究动机。 1 2 1w e b 服务组合建模 当前有关w 曲服务组合建模的研究【2 l 】都是采用某种形式化规约对w 曲服务组合的交互过程进行建 模。主要采用的形式化规约包括有限状态机，2 3 ，2 4 1 、舻演算贮5 ，2 6 1 和p e 仃i 网1 2 7 1 。这些方法各有优缺点， 如有限状态机的语义比较清晰，容易用来进行验证，但对并发能力描述不足；p e 仃i 网则对模型的组合 性描述不足：而舻演算的表达力较强，但其表示方式不够直观，不易理解。尽管以上三种形式化模型 的理论基础、表达力等方面各不相同，但在对于w 曲服务组合建模而言，其建模能力基本相当，只是 在各自使用的方便程度以及计算复杂度方面还是存在差异。 总体来说，这些方法有两个方面的缺陷：其一是直接将w 曲服务组合规约映射到形式化模型，然 而当w 曲服务组合规约不存在时，这些方法很难帮助设计者直接建立服务组合的形式化模型；其二是 仅仅对服务组合的行为进行建模，而忽略了如何对组合过程中数据流信息进行建模，从而不能用于后续 验证数据属性。 所以，在已有工作的基础上，需要提出一种表示和形象刻画w 曲服务组合规约的方法。同时，在 建模的过程中，加入充足的表示数据流的语义信息，用于后继的数据属性的验证。 1 2 2w e b 服务组合的静态验证 多数静态验证w 曲服务组合方法的基本思想都是从组合规约中获取行为模型，作为某个验证工具 的输入进行验证。这些方法仅仅考虑了组合规约的行为正确性，未考虑数据流问题。然而，行为正确性 并不能保证数据属性的正确性。与行为属性相比( 安全性和活性) ，与数据相关的属性是隐含的和