（计算机科学与技术专业论文）基于分层着色petri网的web服务动态组合建模与验证.pdf

- 一 一 h i e r a r c h i c a lc o l v e r i f i c a t i o nf o r a t h e s i s c a n d i d a t e ：s u nl i a n x i a s u p e r v i s o r ：z h ul i a n z h a n g c o l l e g eo fc o m p u t e r c o m m u n i c a t i o ne n g i n e e r i n g c h i n au n i v e r s i t yo f p e t r o l e u m ( e a s t c h i n a ) 煳聊 本人郑重声明：所呈交的论文是本人在指导教师指导下独立进行研究t 作所取得的 成果，论文中有关资料和数据是实事求是的。尽我所知，除文中已经加以标注和致谢外， 本论文不包含其他人已经发表或撰写的研究成果，也不包含本人或他人为获得中国石油 大学( 华东) 或其它教育机构的学位或学历证书而使用过的材料。与我一同工作的同志 对研究所做的任何贡献均己在论文中作出了明确的说明。 若有不实之处，本人愿意承担相关法律责任。 学位论文作者签名： 同期：加f 年歹月3 汐e l 学位论文使用授权书 本人完全同意中国石油大学( 华东) 有权使用本学位论文( 包括但不限于其印 刷版和电予版) ，使用方式包括但不限于：保留学位论文，按规定向国家有关部门( 机 构) 送交学位论文，以学术7 ：乏流为目的赠送和交换学位论文，允许学位论文被查阅、 借阅和复印，将学位论文的全部或部分内容编入有关数据库进行检索，采用影印、 缩印或其他复：叫于段保存学位论文。 保密学旺论文在解密后的使用授权同上。 学位论文作者签名：型! 显鱼 指导教师签名： 维选聋 日期：知f f 年岁月步日 日期：砌年多月扣日 摘要 随着w e b 服务技术的发展，网上发布的w e b 服务的数量将越来越多，当单个服务 无法满足用户的需求时，需要将多个功能有限的服务进行服务组合，产生增值服务。手 工地去组合这些w e b 服务，不便于对服务组合依据用户需求变化，进行动态调整，所 以迫切需要对这些服务进行动态组合。w e b 服务本体描述语言o w l s 所描述的w e b 服务流程，使得w e b 服务包含机器可读的语义信息，可以实现w e b 服务的自动发现、 组合、执行和监控。但动态服务组合却是一个复杂而易错的过程，现有的组合规范缺乏 有效的验证机制，因此需要建立w e b 服务组合的形式化描述模型，利用对形式化模型 的分析，验证方法来检验w e b 服务动态组合的正确性和有效性。 目前已有一些形式化验证方法，主要有基于进程代数、自动机和p e t f i 网。但是进程 代数和自动机方法只是停留在语法层面，对语义信息描述不够，且建模过程复杂，模型 抽象，缺乏直观的图形表示。由于基本p e t r i 网没有颜色和分层的概念，不能精确表达w e b 服务不同类型的数据，而且对于大规模复杂系统，容易出现状态空间爆炸问题。 本文提出一种利用分层着色p e t r i 网( h c p n ) 对以o w l s 描述的w e b 服务组合流程 建模和验证的方法。首先研究基于o w l s 的语义w e b 服务动态组合流程，得到w e b 服务组合过程模型；然后提出o w l s 描述的w e b 服务组合流程中的原子过程，复合过 程以及各控制结构向p e t r i 网转化的规则，得到w e b 服务动态组合过程模型对应的分层 着色p e t r i 网模型；最后利用c p nt o o l s 工具对建立的c p n 模型进行动态模拟仿真，并 通过状态空间机制验证模型的有界性、可达性、活性( 探测有无死锁) 等各项性能。从 而达到验证w e b 服务组合正确性和有效性的目的。 分层着色p e t d 网( h c p n ) 建模，弥补了一般p e t r i 网的不足，引入不同颜色的t o k e n 以及t o k e n 数的变化来表示o w l s 模型中的i o p e ，可以更好的刻画w e b 服务的控制 流和数据流，引入分层概念，可以简化模型，对于大型复杂系统可以分成一些子网，每 个阶段独立验证，逐步求精，对于有相同结构的子网，不必重复建模。同时也有利于避 免状态空间爆炸问题。 关键词：w e b 服务组合，w e b 服务本体描述语言，h c p n ，建模，验证 r h i e r a r c h i c a lc o l o r e dp e t r in e t sb a s e dm o d e l i n ga n dv e r i f i c a t i o nf o r d y n a m i c w e bs e r v i c ec o m p o s i t i o n s u nl i a n x i a ( c o m p u t e rs c i e n c e & t e c h n o l o g y ) d i r e c t e db yp r o f e s s o rz h ul i a n z h a n g a b s t r a c t w i t ht h ed e v e l o p m e n to fw e bs e r v i c e st e c h n o l o g y , m o r ea n dm o r ew e bs e r v i c e sh a v e b e e np u b l i s h e do nt h ei n t e r n e t w h e na ni n d i v i d u a ls e r v i c ec a nn o tm e e tt h en e e d so fu s e r s ，i t i sn e c e s s a r yt oc o m p o s es e v e r a lf u n c t i o nl i m i t e ds e r v i c e s ，s ot h a ti tc a np r o d u c ev a l u e a d d e d s e r v i c e s m a n u a lc o m b i n a t i o no fw e bs e r v i c ec a nn o td y n a m i c a l l ya d j u s tw e bs e r v i c e s c o m p o s i t i o np r o c e s sa c c o r d i n gt ot h ec h a n g e so fu s e rn e e d s ，s ot h e r ei sa nu r g e n tn e e df o ra d y n a m i cc o m b i n a t i o no ft h e s ew e bs e r v i c e s w e bs e r v i c e sp r o c e s s e sd e s c r i b e db yw e b o n t o l o g yl a n g u a g eo w l sc a nm a k ew e bs e r v i c e si n c l u d em a c h i n eu n d e r s t a n d a b l es e m a n t i c i n f o r m a t i o n ，t h u si tc a nl e a dw e bs e r v i c e st or e a l i z et h ea u t o m a t i cd i s c o v e r y , c o m p o s i t i o n ， e x e c u t i o na n dm o n i t o r i n g b u tt h ed y n a m i cw e bs e r v i c e sc o m p o s i t i o ni sac o m p l e xa n d e r r o r - p r o n ep r o c e s s f o rl a c k i n go fe f f e c t i v ev e r i f i c a t i o nm e c h a n i s m ，i ti sn e c e s s a r yt o e s t a b l i s hf o r m a ld e s c r i p t i o nm o d e lo fw e bs e r v i c e sc o m p o s i t i o n ，a n dt h r o u g ht h ea n a l y s i sa n d v e r i f i c a t i o no fm o d e l st ov e r i f yt h ec o r r e c t n e s sa n de f f e c t i v e n e s so fd y n a m i cw e bs e r v i c e s c o m p o s i t i o n t h e r ea r ea l r e a d yf o r m a lv e r i f i c a t i o nm e t h o d sh a v eb e e np r o p o s e d ，m a i n l yb a s e do n p r o c e s sa l g e b r a ，a u t o m a t aa n dp e t r in e t s b u tt h ep r o c e s sa l g e b r aa n da u t o m a t am e t h o d sa r e o n l yi nt h es y n t a xl e v e l ，t h e yh a v en o te n o u g hs e m a n t i cd e s c r i p t i o nf o rw e bs e r v i c e ，a l s ot h e y h a v e c o m p l e xm o d e l i n gp r o c e s s ，a n d t h e a b s t r a c tm o d e l sl a c ko fi n t u i t i v e g r a p h i c a l r e p r e s e n t a t i o n b e c a u s eb a s i cp e t r in e t sw i t h o u tc o l o ra n dh i e r a r c h i c a lc o n c e p t ，s ot h em e t h o d c a nn o te x p r e s sd i f f e r e n tt y p e so fd a t ao fw e bs e r v i c e sa c c u r a t e l y , a n df o rl a r g e s c a l ea n d c o m p l e xs y s t e m s ，i ti se a s yt ol e a ds t a t es p a c ee x p l o s i o np r o b l e m i nt h i sp a p e r ，b a s e do nt h es e m a n t i c so fw e bs e r v i c e so n t o l o g yl a n g u a g eo w l s ，a m o d e l i n ga n dv e r i f i c a t i o nm e t h o du s i n gh i e r a r c h i c a lc o l o r e dp e t r in e t s ( h c p n ) f o rw e b s e r v i c e sc o m p o s i t i o np r o c e s s e si sp r o p o s e d f i r s to fa l li tr e s e a r c h e st h es e m a n t i cw e bs e r v i c e d y n a m i cc o m p o s i t i o np r o c e s sb a s e do no w l s ，a n dg e tw e bs e r v i c ec o m p o s i t i o nm o d e l r r e p r e s e n tt h ei o p eo ft h eo w l sm o d e l ，t h ec o n t r o lf l o wa n dd a t af l o wo fw e bs e r v i c e sc a n b ec h a r a c t e r i z e db e t t e r t h ei n t r o d u c t i o no fh i e r a r c h i c a l c o n c e p t ，w h i c hc a ns i m p l i f yt h e m o d e l ，f o rl a r g e s c a l ea n dc o m p l e xs y s t e m s ，i tc a nb ed i v i d e di n t os e v e r a ls u b n e t s ，g i v ea n i n d e p e n d e n tv e r i f i c a t i o nf o re a c hs t a g e ，s t e pr e f i n e m e n t i fs o m es u b n e t sh a v es a m es t r u c t u r e ， t h e r ei sn on e e dt or e p e a tt h em o d e l i n gp r o c e s s ，a l s oi th e l pt oa v o i ds t a t es p a c ee x p l o s i o n p r o b l e m k e yw o r d s ：w e bs e r v i c ec o m p o s i t i o n ，w e bs e r v i c e so n t o l o g yl a n g u a g e ，h c p n ，m o d e l i n g ， v e r i f i c a t i o n 目录 第一章绪论1 1 1 课题研究的背景及意义1 1 2 国内外研究现状2 1 3 研究内容和研究路线。5 1 3 1 研究内容5 1 3 2 研究路线6 1 4 论文的组织结构7 第二章w e b 服务及w e b 服务组合技术简介9 2 1w | e b 服务技术9 2 1 1w e b 服务定义及特点9 2 1 2w e b 服务标准一1 0 2 1 3w e b 服务体系结构11 2 2w e b 服务组合技术1 2 2 2 1w e b 服务组合分类。1 3 2 3w 曲服务动态组合基础1 5 2 3 1 本体论15 2 3 2 语义w e b 服务17 2 3 3w e b 服务本体描述语言( o w l s ) 1 8 2 4 本章小结2 0 第三章着色p e t r i 网概述2 2 3 1 基本p e 研网2 2 3 1 1p e 仃i 网定义2 2 3 1 2p e t r i 网基本结构2 4 3 1 3p e t r i 网基本性质。2 4 3 2 着色p e t r i 网2 5 3 2 1c p nj 定义2 5 3 2 2c p n 的层次化模型2 6 3 3 建模工具c p nt o o l s 简介2 8 3 3 1c p nt o o l s 仿真工具3 0 3 3 2c p nt o o l s 状态空间工具3 1 3 4 本章小结3 3 第四章o w l s 服务组合模型到c p n 模型的转化3 4 4 1o w l s 服务组合模型到c p n 模型的转化规则3 4 4 1 1o w l s 原子过程到c p n 的转化3 5 4 1 2o w l s 复合过程到c p n 的转化3 5 4 2w e b 服务组合模型验证分析4 2 4 3 本章小结4 3 第五章实例模型构建与验证4 4 5 1 医院就诊服务流程4 4 5 2 医院就诊服务流程对应的c p n 模型4 6 5 2 1 主流程的c p n 模型4 6 5 2 2 挂号服务( r e g i s t e r ) 子页面4 7 5 2 3 诊断服务( d i a g n o s e ) 子页面4 8 5 2 4 检查服务子页面4 9 5 2 5 非住院治疗服务( u n h o s p i t a l i s e dt r e a t m e n t ) 子页面5 0 5 2 6 住院治疗服务( h o s p i t a l i z e dt r e a t m e n t ) 子页面51 5 3 组合模型的正确性和有效性验证5 2 5 3 1 模型的仿真分析5 3 5 3 2 模型的状态空间分析5 4 5 4 本章小结5 6 结论与展望5 8 参考文献。6 0 攻读硕士学位期间取得的学术成果6 4 致 射6 5 中国石油大学( 华东) 硕士学位论文 1 1 课题研究的背景及意义 第一章绪论 随着w 曲服务技术的发展，网上发布的w 曲服务的数量将越来越多，当单个服务无 法满足用户的需求时，需要将多个功能有限的服务进行服务组合，产生增值服务，以满 足复杂业务的需要【1 1 。w 曲服务组合能够使得小粒度w r e b 服务通过相互通信和协作，组 装成大粒度w 曲服务；并可通过整合各种功能不同的w 曲服务，来解决比较复杂的需要 多个服务组合起来才能解决的问题，从而实现其增值功能【2 l 。但是这些w 曲服务的更新 很快，而且手工地去组合这些w 曲服务，也不便于对服务组合依据用户需求变化，进行 动态调整。所以基于w 曲服务的动态服务组合作为实现灵活、快速信息集成的重要方法， 成为新的研究热点。但动态服务组合却是一个复杂而易错的过程。设计有误的组合服务 一旦付诸实施，将会造成比较大的损失，因为这些错误通常会造成资源和时间的巨大浪 费。所以为了在组合服务执行前能够及时发现并修改错误，并将执行时因错误而造成的 损失降到最低，有必要在组合规划时对组合服务进行正确性分析和验证。对w 曲服务组 合进行分析和验证的主要目的就是保证即使在复杂度高的情况下，也能构造出正确可靠 的服务组合，并且在w | e b 服务组合真正投入实施前能够及时发现并修改潜在的设计错 误。因为要达到这个目标所利用的方法就是建立w 曲服务组合流程的形式化描述模型， 通过对建立的形式化模型进行分析和验证，从而检验w 曲服务动态组合的正确性和有效 性【3 】，保证组合服务的顺利执行。p e t r i 网作为一种基于状态的形式化建模方法，具有直 观、形象且有严格语义和数学分析之优点，是理想的数据流和控制流的抽象、形式化建 模方法。 为了理解并使用一个w e b 服务，软件实体需要一个计算机可解释的服务描述。语 义w e b 可看成是当前w 曲技术的一个延伸和扩展。语义w e b 4 是由一些能够被计算机 直接或间接处理的数据组成的w e b 。其思想是通过本体( o n t o l o g y ) 和w e b 内容的语义标 记，使计算机能够理解并自动处理w e b 上的内容，从而更有助于计算机之间以及计算 机与人之间的协同工作，方便人们在w e b 上发现知识和处理事物。 w e b 服务作为w e b 上的一类越来越重要的资源，需要语义对w | e b 服务提供广泛的 语义支持。o w l s 是基于o w l 本体语言的w e b 服务本体，定义了一组核心语言构件， 用于对w e b 服务进行逻辑化描述，所生成的描述文件支持机器理解，从而支持动态服 第一章绪论 务组合，实现对w e b 服务的自动发现，调用，组合、执行和监控，并且能够提供非功 能性的属性描述【5 j 。 但是目前基于语义的w e b 服务动态组合的形式化建模验证的研究还比较少，所以 本论文主要是对o w l s 所描述的语义w e b 服务动态组合的建模和验证，通过将o w l s 所描述的w e b 服务组合流程转化成具有相同语义的着色p e t r i 网模型，然后利用c p n 成熟的分析工具c p nt o o l s 对转化后的c p n 模型进行动态模拟服务调用执行情况，考 察是否能得到用户需要的输出；并利用状态空间工具，计算状态空间生成图，生成状态 空间报告来分析验证有界性、可达性、活性等动态行为特性以达到验证服务组合逻辑和 功能上正确性的目的。本文还引入了层次网的概念，采用自顶向下逐步分解描述和自底 向上逐步综合替代的方法构造分层p e t r i 网，这样对于有相同结构的子网，不必重复建 模和分析，而且模型结构简单直观，便于对其性质进行分析和处理，有利于各个阶段的 独立验证和确认。对于复杂的大型系统，可以简化整个验证过程，有效避免了状态空间 爆炸问题。 1 2 国内外研究现状 当前国内外对w 曲服务动态组合的建模与验证的研究都比较积极，主要有针对业务 流程的验证方法，也有针对在语义网络下w e b 组合的验证方法，因为动态组合方式有多 种，对于不同种类组合方式，有不同验证方法。有三种典型的方法：基于进程代数、基 于p e t r i 网和基于有限自动机f s m 。下面分别叙述下这三种方法现有的研究成果。 1 基于自动机的w 曲服务组合验证方法。基于有限自动机理论的方法是一种常用 的形式化验证方法，该方法的基本思想是采用自动机描述服务交互过程中的信息交换序 列，从而模拟w 曲服务组合过程中的状态和操作，同时利用时序逻辑将系统的目标属性 描述成断言，然后通过模型检测方法判断组合服务是否满足用户预先定义的需求。 n a k a j i m a 【6 】提出采用s p i n 模型检测器来验证基于编制的组合w e b n 艮务的正确性，将基于 w s f l 语言描述的组合w e b 服务转换为s p i n 模型，然后使用l t l 线性时序逻辑公式来表 达需要验证的服务属性，最后通过模型检测器验证了组合服务的正确性。k a r 锄a j l o l i s 【7 】 将抽象组合w r e b 服务转换为f s p 过程，并使用l t s a t _ 具进行验证。类似的，f o s t e r l 8 】将 b p e l 语言描述的组合服务转化为f s p 过程，并使用l t s a i 具进行验证。k o e h l e r 【9 】将组 合w 曲服务的抽象业务流程转化为具有状态迁移变量和变迁安全警卫( g u a r d ) 的非确定自 动机，然后将自动机被转换为模型检测器的输入，从而利用模型检测器进行验证。文献 2 中国石油大学( 华东) 硕士学位论文 【1 0 】利用线性逻辑对自动语义w | e b 服务提供了一种解决的方法。在这种方法中，w 曲服务 和客户的需求都由d a m l ss e r v i c e p r o f i l e 来说明。这类方法优点是对于规模较小的服务 组合，可以模拟w 曲服务组合的状态和操作，最适用于自动组合的情况。缺点是公式计 算较复杂而且缺乏直观的图形化表示。 2 基于进程代数的w e b 服务组合验证方法。进程代数是一类采用代数的形式描述 并验证系统的理论的总称。它是一种可以描述并且推理进程行为、对动态实体进行建模 的形式化语言，具有严密的形式化语义。它包括通信系统演算( c a l c u l u s o f c o m m u n i c a t i n gs y s t e mc c s ) 【1 1 】，通信顺序进程( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s c s p ) 以及p i 演算等。s c h r o e d e r 【1 4 1 提出将组合w 曲服务的抽象业务流程转换为 c c s ，然后使用已有的验证工具c w b 来验证流程的正确性。文献【l5 j 使用c c s 描述w e b 服务编排接口w s c i ，并验证两个或者更多的w r e b 服务能否行为兼容。文献【1 6 】采用p i 演算对用b p e l 描述的w e b 服务组合流程进行建模，并通过p i 演算的操作语义和推理 能力判断w e b 服务间信息交互的兼容性和逻辑结构的正确性。此类方法优点是可以提 供简单和形式化的定义来表示w e b 服务间进行交互的消息，适用于有并发和通信组件 组成的系统，其中p i 演算还提供了以顺序的，并发的和条件的执行形式以及组合，这 些能够构造任意复杂组合的活动【1 7 】。但这种方法公式计算复杂，容易出错，而且同样缺 乏直观的图形化模型。 3 基于p e t r i 网的w 曲服务组合验证方法。p e t r i 网能够对系统的状态和操作进行形式 化地描述，便于对系统进行建模分析和验证，对于描述离散事件动态系统具有较强的模 型分析能力【1 8 1 。现在研究比较多的是使用p e t r i 网来对w 曲服务组合进行验证。目前利用 p e t r i 网验证w e b 服务组合流程已经出现了诸多代表性的工作，他们分别针对组合w 曲服 务的不同方面进行验证。h a m a d ir ，b e n a t a l l a hb 1 1 9 针对抽象组合w _ e b 服务，提出利用p e t r i 网描述1 0 种w | e b 服务组合的基本模型，利用代数元模型描述服务组合控制流，同时建立 了从代数元模型向p e t r i 网转化的映射机制，从而为服务组合过程中的服务功能或非功能 属性验证，以及组合服务执行过程的检测和优化提供了一种形式化验证工具。但是对于 o w l s 所描述的w e b l l 务组合流程缺乏有效的转换机制。n a r a y a n a ns ，m c l l r a i t hs t 2 0 1 提 出使用d a ) a 服务代理标记语言( d a r p a a g e n tm a r k u pl a n g u a g ef o rs e r v i c e ，d a m l s ) 本体描述w | e b 服务，其组合和验证的方法是首先将d a m l s 所描述的服务组合模型映射 到情境演算，然后再映射至t p e t r i 网。首先定义了顺序、并行、选择、循环等6 种基本组 合方式，然后在可用w 曲服务的组合网中找到满足用户目标需求的一种组合，最后通过 3 第一章绪论 对p e t r i 网的性质分析达到对组合服务分析和验证的目的。但是这种方法不能够精确表达 w r e b 服务的不同类型的资源数据。a n d o n o f f ，b o u z g u e n d a ，h a n a c h i t 2 l j 提出基于对象p e t r i 网( p e t r in e t sw i t ho b j e c t s ，p n o ) 组合w 曲服务的方法，将w 曲服务映射到一个p n o 系统， 然后通过消息传递机制将不同的网系统集成到一起，形成组合服务和服务之间的控制 流。k o s c h m i d e r a ，m e v i u sm 【2 2 】提出使用可扩展标记语言( e x t e n s i b l em a r k u pl a n g u a g e ， x m l ) 对业务流程之间的协作关系进行建模，并且提取了其中的业务流程执行语言 ( b u s i n e s sp r o c e s se x e c u t i v el a n g u a g e ，b p e l ) 元素。首先业务流程语言描述的组合并不 是真正意义上的动态组合，其次用x m l 网验证也缺少形式化的语义。y ix i a o c h u a n ， k o c h u t jk 【2 3 】提出使用c p n e t 对基于b p e l 4 w s 的服务组合系统进行验证。文献【2 4 】也是对 于b p e l 4 w s 所描述的w 曲服务流程进行了针对结构框架元素部分的p e t r i 网模拟与验证。 但是b p e l 4 w s 所描述的w | e b 服务流程仅限于语法层次的表达，对服务语义信息描述不 够，不是真正意义上的动态服务组合，因此其验证技术也只能局限于检测设计期组合错 误。而本文采用的o w l s 能精确描述w 曲服务的语义信息，从而提供了自动组合的可能 性。郭玉彬，杜玉越【2 5 】等提出着色p e t r i 网的代数模型，将原子服务形式化描述成p e t r i 网 模型，然后利用提出的代数运算法则将原子服务组合成复合w 曲服务。由于p e t r i 网具有 丰富的数学理论分析方法，因此可以对组合服务进行定性分析和验证其正确性。但是这 种方法没有涉及到w | e b 服务的语义表示，不能进行动态组合，也没有给出具体的验证组 合服务正确性的方法。文献【2 6 】提出了利用着色p e t r i 网对w 曲服务动态组合的基本模式进 行形式化建模和分析的方法。但没有从整体上给出w 曲服务组合流程的p e t r i 网表示和验 证方法。钱柱中，陆桑璐【2 7 】等提出利用面向消息的基于行为p e t r i 网对w e b 服务建模，该 模型既能够根据消息传递机制完成服务间的通信，又能够对服务行为给出过程描述，然 后利用组合规则实现了w 曲服务的自动组合。但是这种方法没有明确描述语义w 曲服务， 也没有将组合流程中的资源纳入建模中，不能全面描述流程。程永上，王志型2 8 1 提出利 用着色p e t r i 网中的t o k e n 来表示语义w 曲服务的不同类型的资源数据，使用带有不同颜色 值的t o k e n 以及t o k e n 数目的变化来表示o w l s 描述的w r e b 服务组合流程模型中的l o p e ， 以此来描述w 曲服务的输入信息、输出信息、前提条件和执行效果。对o w l s 描述的服 务组合流程中的原子过程，复合过程以及各控制结构都给出了p e t r i 网模拟，并对组合模 型的正确性、有界性、可达性和活性进行了验证。但是对于结构复杂的组合流程的验证 没有给出解决办法。 上述介绍了国内外对于w e b 服务动态组合的验证的研究，可以看出基于自动机的 4 中国石油大学( 华东) 硕士学位论文 方法可以描述w e b 服务需要验证的属性，但是描述服务组合的行为不够直观，建模比 较困难，采用进程代数则公式计算较复杂，同样也缺乏直观的图形表示。所以大多方法 还是基于p e t r i 网的，主要是因为p e t r i 网不仅能对系统的静态结构进行刻画，而且可以 对系统的动态行为进行模拟：不仅具有直观的图形化表示方法，而且能够引入许多数学 方法对模型性质进行分析，并进行正确性验证。作为形式化的描述和分析验证工具，p e t r i 网特别适合对并发和分布式系统进行描述，并对系统进行定性和定量分析。但是上述方 法大多还是基于基本p e t r i 网，没有数据和分层概念，因此不能精确表达w e b 服务的语 义，或者不能将控制流和数据流结合在一起描述，也不适合刻画大型复杂的系统。因为 分层着色p e t r i 网对基本p e t r i 网在数据和层次方面进行了扩展，可以对大型复杂系统建 立简单直观的层次化c p n 模型。它是将复杂系统分成一些子网，每个阶段独立验证， 逐步求精，同时可以表示语义w e b 服务的不同类型数据，对系统行为进行动态模拟和 形式化验证，弥补了一般p e t r i 网的不足，另外o w l s 描述w e b 服务服务，可以利用 语义描述和本体逻辑推理，实现w e b 服务的自动发现、选择、调用、组合、执行监控 等，实现真正意义的动态服务组合。所以本文提出了利用分层着色p e t r i 网对o w l s 描述的w e b 服务组合流程建模。 1 3 研究内容和研究路线 1 3 1 研究内容 l 、w | e b 服务及语义w e b 服务 学习和研究w e b 服务相关的协议和标准。w e b 服务是以x m l 格式的数据标准为基 础的应用，其使用的协议是标准协议且具有开放性：包括w e b 服务描述语言( w s d l ) ； 简单对象访i h 协议( s o a p ) ；统一描述、发现和集成协议( u d d i ) t 1 7 1 。 语义w e b 服务( s e m a n t i cw e bs e r v i c e ) 是语义w e b 和w e b 服务的结合，目前语义 w e b 服务的主要方法是利用本体来描述w e b 服务，o w l - s ( o m o l o g yw e bl a n g u a g ef o r s e r v i c e s ) 是用o w l 语言描述的语义w e b 服务的本体，使用o w l s 的w e b 服务构架结 合已有的( s o a p ，w s d l ，u d d i ) 可以实现w e b 服务的发现、执行和组合自动化。 2 、基于o w l s 的语义w | e b 服务动态组合 研究基于o w l s 所描述的语义w e b 服务的原子过程，组合过程( 含有控制结构的 子过程) 及数据流的过程模型。这里主要研究原子过程如何接受输入信息和服务的前提 条件，使用控制构件( c o n t r o lc o n s t r u c t ) 女ns e q u e n c e ，i f - t h e n e l s e 等得到输出和执行效果。 s 第一章绪论 了解了过程模型，可以有助于下一步制定相应的映射规则，把组合的过程模型映射到 p e t r i 网进行验证分析。 3 、语义w e b 服务组合的过程模型向分层着色p e t r i 网的映射 根据语义w e b 服务的原子过程操作语义描述，即根据输入信息、输出信息、前提 条件和执行结果( i o p e ) 锘i 定相应的映射规则，可以有多个输入和多个输出，建立相应的 着色p e t r i 网模型。对组合过程的控制结构再建立相应着色p e t r i 网模型，从而任何一个 复杂的组合系统模型，都可以由原子服务通过各控制结构以及相应的语义信息复合而 成，复合服务是原子服务或其他复合服务。所以都可以建立相应的分层着色p e t r i 网模 型。 4 、利用分层着色p e t r i 网对组合后的模型进行模拟和验证 利用上述映射规则对一个组合后的过程模型建立分层着色p e t r i 网后，就可以利用 c p nt o o l s 工具来模拟仿真服务的调用执行情况，并可通过仿真报告分析能否得到用户 期望的输出，验证服务组合的有效性；同时可以利用c p nt o o l s 工具的状态空间机制得 到状态空间报告和可达性图验证组合过程模型的有界性、可达性、安全性、活性( 探测 有无死锁) ，从而达到验证w e b 服务组合流程正确性的目的。利用着色p e t r i 网的分层 模型，可以对复杂的系统模型，将其分为许多子网，也就是对组合服务的任何子服务( 原 子服务或者组合服务) 通过自顶向下的服务分解的方法分层逐步验证，大大简化了整个 流程验证过程。 1 3 2 研究路线 本课题采用理论研究与技术研究并举的基本路线。 1 从对w e b 服务的协议标准和w e b 服务的体系结构以及语义w e b 服务的本体描 述语言的学习、分析、总结入手，结合已有的语义w e b 服务动态组合方法及验证机制， 提出一种利用分层着色p e t r i 网来验证基于o w l s 描述的语义w e b 服务动态组合过程 模型的方法。 2 利用现有的语义w e b 服务本体语言o w l s 的规范及所描述的语义信息( 输入 信息、输出信息、前提条件和执行结果) 及w e b 服务的原子过程、组合过程( 含控制 结构的子过程) ，也就是从数据流和控制流两个维度出发建立相应的分层着色p e t r i 网模 型，在此基础上可以对任何一个复杂的组合过程模型建立相应的分层着色p e t r i 网模型。 3 最后利用现有的c p nt o o l s 工具模拟过程模型的动态性，并验证有界性、可达 6 1 4 论文的组织结构 图1 - 1 技术路线图 f i g l - 1 t h et e c h n o l o g yr o u t e 全文共分为五章，具体的组织结构如下： 7 第一章绪论 第一章主要介绍了研究动态服务组合建模和验证的目的和意义。分析了当前国内外 对w e b 服务动态组合的建模与验证的研究现状，同时比较了服务组合建模与验证方面 各方法的优缺点，提出了本课题的研究内容和研究路线。 第二章主要介绍了w e b 服务技术、w e b 服务组合技术以及动态w e b 服务组合相关 技术理论，通过分析这些基础理论，引出本文研究方向是利用形式化的方法，对基于 o w l s 描述的w e b 服务的动态组合流程进行建模分析和验证。 第三章介绍了基本p e t r i 网以及c p n 的相关理论和分析方法，简单说明了c p n 建 模工具c p nt o o l s 的使用方法。重点介绍了c p nt o o l s 的仿真分析和状态空间分析方法。 这为后文利用c p n 对w e b 服务组合流程建模与验证奠定了基础。 第四章是本文的重点，根据w e b 服务组合流程与p e t r i 网的语义相似性，提出了 o w l s 原子过程和组合过程模型向c p n 模型的转化规则。重点介绍了o w l s 组合过 程中的几种控制结构对应的相同语义的c p n 模型结构。并且在o w l s 原有的基本控制 结构的基础上又进行了扩展，这样使得服务组合流程对应的c p n 模型语义更加丰富。 最后在服务组合模型的基础上，分析了c p n 模型的有界性、可达性、活性在w e b 服务 组合中表示的意义。 第五章通过医院就诊服务流程的具体实例说明了如何利用c p nt o o l s 对w e b 服务 组合流程进行建模和验证。包括流程模型的建立，层次c p n 模型的获取和利用c p n t o o l s 分析工具对建立的c p n 模型进行仿真分析和状态空间分析，模拟验证c p n 模型 的各项性能，从而模拟和验证组合流程的正确性和有效性。 最后部分为整篇论文的总结，以及今后工作的展望。 8 中国石油大学( 华东) 硕士学位论文 第二章w e b 服务及w e b 服务组合技术简介 2 1w e b 服务技术 w e b 服务是现有应用面向i n t e m e t 的一个延伸，