基于Petri网的Web服务组合模型描述和验证

1、统 仿 真 学 报 V ol. 19 No. 122007年6月 Journal of System Simulation Jun., 2007第19卷第12期 系基于Petri 网的Web 服务组合模型描述和验证张佩云, 黄 波, 孙亚民(南京理工大学计算机科学与技术学院, 南京 210094摘 要：Web 服务及其组合的形式化描述和验证是Web 服务中一个重要的研究方向。分析了基于Petri 网建模的优势，给出基于Petri 网的Web 服务的形式化定义和描述，对Web 服务组合进行建模及元素映射，给出Petri 网模型生成算法并对组合服务模型的可达性、安全性、有界性与活性等特性进行验证分

2、析。最后是对一个具体的业务流程的建模和验证分析。由分析可知，该建模方法具有一定的表达和验证Web 服务组合模型的能力。关键词：Web 服务；Petri 网；服务组合；服务组合验证中图分类号：TP391 文献标识码：A 文章编号：1004-731X (2007 12-2872-05Petri-Net-Based Description and Verificationof Web Services Composition ModelZHANG Pei-yun, HUANG Bo, SUN Ya-min(School of Computer Science & Technology, Nanjin

3、g University of Science & Technology, Nanjing 210094, ChinaAbstract: Formal description and verification of web services and their composition are important research issues. The advantages were discussed for modeling web services composition using Petri net. Based on Petri net theory, the formal def

4、inition and graphic description were proposed for web services and their composition; the element mapping process was also illustrated. Then an algorithm was proposed to construct the Petri net model for web services composition. The reachability, safeness, boundness and liveness of the model were a

5、lso validated. As an example, a concrete web services composition for a system was modeled and validated based on Petri net method, it showed that this modeling approach has enough capability in expressing and verifying web services composition.Key words: web services; Petri net; services compositio

6、n; services composition verification引 言Web 服务是语义网的一个关键应用研究领域， Web服务的激增和语义网技术的发展，为多样的Web 服务组合提供了便利。语义网技术提供了计算机可判断的Web 内容和性能标记，推动了服务的自动发现和服务组合。目前Web 服务及其组合的形式化描述和验证是语义Web 服务中一个重要的研究方向，现有的许多Web 服务及其组合描述语言都是半形式化的，容易出错和不容易检测，正确性难以保证，需要有形式化的方法来验证Web 服务组合模型1。模型的正确性是指模型结构上的正确性，即是安全、有界、无死锁等。Petri 网作为一种基于状态的形

7、式化建模方法，具有直观、形象且有严格语义和数学分析之优点，是数据和控制流的抽象和形式化建模方法。本文采用Petri 网对Web 服务组合进行描述和正确性验证。Management and Business Process Management和Web 服务组合语言上下文环境中，Petri 网和Pi 演算的最优性上存在着争论。文献2认为Petri 网在Web 服务建模上具有Pi 演算不具备的优点，Petri 网能对包含结构的复杂系统建模，而Pi 演算不能对之进行建模。Petri 网是一个良好的过程建模方法，一个Petri 网是一个定向连接的双向图，图中节点代表库所和变迁3。Petri 网有严格的

8、数学基础，可以广泛应用于描述和研究具有并发、异步、分布、并行、非确定性和随机性质的信息系统，提供了一种可操作语义及定性和定量分析4。在比较分析了建模方法后，本文采用Petri 网对Web 服务组合建模分析。2 基于Petri 网的Web 服务组合2.1 基于Petri 网的Web 服务定义为了应用Petri 网验证Web 服务，需将Petri 网元素与Web 服务的元素相对应，以达成用Petri 网形式化地描述Web 服务组合。基于Petri 网的Web 服务定义如下。定义1. Web 服务定义。一个Web 服务S 定义为六元组：S=(Id, SName, Desc, SOnto, URL,

9、Oper，其中：Id ：Web 服务的唯一的标识； SName ：Web 服务的名称； Desc ：服务的描述；1 Web服务组合建模方法分析在过程敏感的信息系统中(如B2B ，CRM ，Workflow收稿日期：2006-05-14 修回日期：2006-11-12 基金项目：高等学校博士点科研基金 (20050288015 作者简介：张佩云(1974-, 女, 安徽安庆人, 博士生, 研究方向为语义网, Web 服务和智能信息处理; 黄波(1980-, 男, 博士, 研究方向为计算机网络技术、Petri 网理论等; 孙亚民(1946-, 男, 江苏张家港人, 教授, 博导, 研究方向为计算机

10、网络技术。2007年6月 张佩云,等：基于Petri 网的Web 服务组合模型描述和验证 Jun., 2007(5 的；(6 S1C S2表示一个组合服务是由S1和S2并发执行后形成的，在并发执行中间两个服务间可能会有通信。组合的Web 服务可以通过上述的代数表达式获得。 定义3. 服务组合模型是合理的，必须满足以下基本要求： (1 每个模型都存在一个输入库所i 和一个输出库所o ；(2 每个变迁库所都在一条从输入库所i 到输出库所o 的路径上；(3 在任何情况下，服务组合总能最终终止，在终止的时候，只有输出库所中有托肯，而其它库所是没有托肯存在的；(4 在组合模型中没有死组合的存在，即任何一

11、个组合都有执行的可能。根据以上四个要求，我们给出组合模型的图形化表示。采用Petri 网建模时，指定服务的操作为变迁，服务的状态为库所，基于Petri 网的Web 服务建模方法中最小的组合单元是原子服务。在服务组合中将子服务(原子服务或组合服务 的操作当作事件(变迁 ，子服务S1和S2的操作执行使得服务的状态(库所 发生了改变。任何时刻一个服务可以处于如下状态：非实例状态(not instantiated、准备好状态(ready、运行状态(running、挂起状态(suspended和完成状态(finished。本文服务组合中处于ready 状态的服务被组合，当服务处于finished 状态时

12、表示服务被组合成功。(1 组合服务S1S2的Petri 网图形化表示如图1所示。 SOnto ：服务的领域本体，包括对服务所属领域类型的语义描述及参数及操作的语义描述；分类领域本体用来过滤掉不相关的不同服务领域的服务，组织服务到服务的所属分类。每个服务领域指向一个特定的服务轮廓本体，在服务组合之前的服务匹配可以借助服务领域本体和特定的服务轮廓本体实现精确的服务匹配。URL ：服务的调用； Oper ：服务的操作集。 定义2. 服务网的定义。一个服务网SN 定义为五元组，用来对服务的动态行为进行建模：SN=(P,T,W,i , o ，其中：P ：有限库所集，代表Web 服务的状态，P= p 1,

13、 p 2,., p n ；T ：有限变迁集，代表服务中的操作(operation及服务之间的操作，T=t 1, t 2,., t n ；W ：(PT (TP ，是有向弧的集合，表示服务状态和操作之间的关系；S 表示一个组合服务是由S 循环执行次后形成i ：输入库所，i =x P T|(x , i W=；o ：输出库所，o . =x P T|(o , x W=；库所i 被认为是服务S 的初始标识，当有一个托肯在库所.i 中时，执行服务S ，当有一个托肯在库所o 中时， 被认为终止服务S 。用标识函数表示系统状态，另外对系统状态的演变过程进行描述，就可以对Web 服务组合系统的静态特性、动态特性进

14、行全面的建模。系统动态演变过程的描述是和Petri 网的运行规则对应的：(1 tT 在标识M 可触发当且仅当对于任何p P ，M(pI(p, t；(2 若t T 在标识M 下可触发，按照激活规则产生新标识M ，M(p=M(p+W(p,t-W(t,p。M 被称为M 的直接可达标存在识，M 称为M 0的可达标识当且仅当在以上运行规则下，一个变迁的触发序列t 1, t 2,., t n ，使得模型标识从M 0转换到M ，所有M 0的可达标识称为Petri 网PN 的可达集。图1 组合服务S1S2(2 组合服务S1S2的Petri 网图形化表示如图2所示。 2.2 Web服务组合的代数描述Web 服务

15、组合组件由原子服务和控制结构两部分组成。控制结构如：顺序、并行、选择、循环等，本文采用Petri 网对控制流精确描述。在定义1的和定义2及文6的基础上， Web 服务组合可通过类BNF 范式的符号进行定义。代数操作符的语法如下：S ：= X| S1S2| S1S2| S1S2 |S | S1C S2 (1 X表示一个原子服务或空服务(即一个服务没有执行任何操作 ；(2 S1S2表示一个组合服务是顺序执行S1和S2后形成的；(3 S1S2表示一个组合服务是执行S1或S2后形成的(不可兼或 ；(4 S1S2表示一个组合服合是按S1和S2顺序执行或按S2和S1顺序执行后形成的，等价于S1S2S2S1

16、；图2 组合服务S1S2(3 组合服务S1S2的Petri 网图形化表示如图3所示。 图3 组合服务S1S2(4 组合服务S 的Petri 网图形化表示如图4所示。2007年6月 系统 仿 真 学 报 Jun., 2007a.选择一个服务状态位置；时用输出弧将状态位置和操作位置的输入变迁相b. 按控制流将此状态分配给相应的服务操作，分配图4 组合服务Sc.连，用输入弧将状态和操作位置的输出变迁相连； 重复Step7，直到按控制流所有操作位置都分配了服务状态。在程序实现中，算法程序的输出就是产生的服务组合的Petri 网模型，它们是用伴随矩阵L +和L -、初始标识M 0、终止标识M f 和操作

17、时间向量来描述的。(5 组合服务S 1C S 2的Petri 网图形化表示如图5所示，两个子服务间有可能有信息通信，库所m 用来存放通信信息。 3.2 应用Petri 网验证Web 服务组合分析Petri 网可采用可达树法、不变量分析、约简等方法，其中可达树分析法直观简捷, 可方便地分析系统的可达性、有界性、活性等各种动态特性，Petri 网的大部分特性可以由可到达树来进行验证。我们通过结合可到达树的构造和正确性的检查来实现流程模型的验证过程。可到达树的基本思想就是将可到达的标识作为节点，变迁的触发作为连接弧，来构造一棵树。我们的算法就是在构造树的过程中，检查服务组合的状态和其中库所的托肯数目

18、以实现流程模型的验证。当服务组合时只关心系统可能的状态时，可达标识集可以满足这类问题的要求。给定Petri 网中的一个标识M ，该网络的可达标识表示为M。给定一个以M 0为初始标识的Petri 网N ，我们可以从M 0(根结点 开始计算得到与使能变图5 组合服务S1C S2对于一些更复杂的服务组合操作，可以由上述基本操作可构成复杂的服务组合操作。如(S1S2SnS ，其Petri 网图形化表示如图6所示。该组合服务表示先执行原子服务集合中的某个Si(i1,2n，再执行S 后形成的组合服务。其中从n 个原子服务中选择最优的原子服务的过程将根据价格，递交时间和可靠性能等因素通过选用一个等级标准来判

19、断。 ready1迁一样多的新标识。从这些新的标识，又可得到更多的标识，重复进行这个过程的结果可得到一棵可达树。节点就是从M 0产生的后继标识，弧代表从一个标识到另一个标识的变迁激发。可达树用来描述从初态M 0开始的所有可能到达的状态，结点代表M 0及其可达的后继，其中树根为M 0，树叶对应着系统的终态，弧代表相应的变迁。从树根到某结点的路径代表着从初态变迁到该状态7。利用可达树算法生成可达树后，任何发生序列都可通过在图上执行搜索获得。Web 服务组合的正确终止对于组合服务非常重要，通过Petri 网对活性和有界性的验证来决定服务是否正常结束，通过是否具有完全可达性、完整性和前进性来验证Web

20、 服务组合的正确性。定义4. 可达性:若从初始标识M 0出发触发一个变迁序列产生标识Mr ，则称Mr 是从M 0可达的。所有从M0可达的标识的集合称为可达标识集或可达集，记为R(M0 。定义5. 有界性:给定PN 以及其可达集R(M0 ，对于位置p P ，若m R(M :M(pk ，则称p 是k 有界的，此处图6 组合服务(S1S2.Sn S3 应用Petri 网分析Web 服务组合正确性3.1 Petri网模型生成算法在服务组合时需要通过Petri 网的分析技术来对组合服务进行验证分析，Petri 网模型生成算法的生成算法如下：Step1. 确定待组合的Web 服务数、各服务的操作以及控制流

21、；Step2. 产生一个的初始服务状态，并加上一个标记，作为初始子网；Step3. for j=1 to M/*待组合服务中有j 个操作模块*/ a.按控制流选择一个操作模块； 足指数分布的概率分布； c.将操作连接到已存在的子网中去。 Step4. end Step5. endStep6. 为每种服务状态创建相应的状态位置； Step7. 使用如下方法将服务状态加入到操作中去： b. 给每个操作分配一个随机操作时间，操作时间满k 为正整数；若Petri 网的所有位置都是k 有界的，则Petri 网是k 有界。在任一个标识M R 定义6. 活性:对于一个变迁t T ，下，若存在某一变迁序列Se

22、r ，该变迁序列的触发使得此变迁t 可触发，则称该变迁是活的。若一个Petri 网的所有变迁都是活的，则称该Petri 网是活的。 2007年6月 张佩云,等：基于Petri 网的Web 服务组合模型描述和验证 Jun., 2007该组合服务是完全可达的。从M 0开始的状态可达集R(M0 =M0,M 1,M 2,M 3,M 4,M 5,M 6,M 7。状态集MS=M0,M 1, M 2,M 3,M 4,M 5,M 6,M 7。因此，对任一个标记M i MS ，均有M i R(M0 ，即组合服务S 1C S 2中任一个状态都是从M 0可达。该组合服务是有界的。在可达树中，每一个位置上的托肯数从未

23、超过2。因此该组合服务是有界的，其上界为2。该组合服务是活性的。从可达树可以看出，从M 0开始，定义7. 完整性:Petri 网所有的状态都是可达的。 定义8. 前进性:每次触发都将逐步推向终态, 可达树中不会出现无论的循环。同时具有上述5个性质的Petri 网不会出现停滞不前的状态，执行中所处的状态及等待的消息是有限的，不会出现死锁(文献8对之有比较详细的证明 。本文给出如下两个Web 服务组合的正确性的分析。(1 组合服务S 1S 2的正确性分析下面通过对图4所示的组合服务S 1S 2的构造可达树，以分析该服务组合的正确性，可达树如图7所示。M i =(i , ready 1, ready

24、 2, finished 1, finished 2, p , o 。M 0 M 1 M 3 4S1Ti T(T是所有变迁的集合 都至少可以被从M 0开始的激发序列激发一次。因此，该组合服务的Petri 网是活性的。该组合服务具有完整性。由可达树可见，组合服务的所有状态都从M 0可达并且可以激发转移到终止状态M 7。该组合服务具有前进性。在可达树中，任意状态之间没有出现无意义的循环。同理，对S1S2、S1S2及 S 的类似分析，可知，这些服务组合同时满足对可达性、有界性、活性、完整性和前进性的要求。M 5= M 6=M 5= M 6=4 基于Petri 网的Web 服务组合的实例分析由于Web

25、 服务的独立性和自治性，当组合多个Web 服务完成一个业务流程时，需要在设计阶段保证组合服务的正确性和效率。下面讨论订单服务业务流程建模和相关服务的组合，Web 服务组合的抽象表示如图9所示。图7 组合服务S1S2的可达树该组合服务是完全可达的。从M 0开始的状态可达集R(M0 =M0,M 1,M 2,M 3,M 4,M 5,M 6。状态集MS=M0,M 1,M 2, M 3,M 4,M 5,M 6。因此，对任一个标记M i MS ，均有M i R(M0 ，即组合服务S 1S 2中任一个状态都是从M 0可达。该组合服务具有界性。在可达树中，每一个位置上的托肯数从未超过1。因此该组合服务是安全的

26、。该组合服务是活性的。从可达树可以看出，从M 0开始，Ti T(T是所有变迁的集合 都至少可以被从M 0开始的激发序列激发一次。因此，该组合服务的Petri 网是活性的。该组合服务具有完整性。由可达树可见，组合服务的所有状态都从M 0可达并且可以激发转移到终止状态M 6。该组合服务具有前进性。在可达树中，任意状态之间没有出现无意义的循环。(2 组合服务S 1C S2的正确性分析构造组合服务S 1C S2的可达树如图8所示。 M i =(i , ready 1, ready 2, finished 1, finished 2, m , o 。 M 0 t1M 1S1M 4M 3M 5M 56t3

27、t3M 7M 7M 7图8 组合服务S 1C S2的可达树图9 Web服务组合抽象表示订单服务接受客户代理的请求并根据订单的数据，调用查询库存数据服务以获取是否有满足客户订单需求的货物，当确认查找到的数据满足客户的需求时，向客户代理发送确定信息，客户代理再通过银行支付服务实现支付操作，订单服务确认客户代理的银行支付已成功，执行向客户发送订单服务完成的操作。具体的服务组合模型如图10所示。用Petri 网该服务组合实例建模时，用到了顺序、选择和循环组合结 图10 Web服务组合实例分析2007年6月 系统 仿 真 学 报 Jun., 2007该组合服务是有界的。在可达树中，每一个位置上的托肯数未

28、超过1。因此该组合服务是安全的。该组合服务是活性的。从可达树可以看出，从M 0开始，构。该Petri 网中库所和变迁的含义如下所示。i 服务的初始标识 p1 客户代理启动成功状态 p2 服务合成辅助状态 p3 订单服务执行状态 p4 服务合成辅助状态 p5 查询库存数据服务成功状态 p6 银行支付服务执行成功状态 p7 订单服务执行成功状态 o 服务的结束状态 t1 启动客户代理操作 t2 订单执行操作 t3 查询库存数据操作t4 查询结果满足订单要求, 返回结果 t5 查询结果不满足订单要求, 结束组合 t6 执行银行支付操作 t7 订单服务执行确认操作 t8 订单执行成功操作Ti T(T是

29、所有变迁的集合 都至少可以被从M 0开始的激发序列激发一次。可见该组合服务的Petri 网是活的。该组合服务具有完整性。由可达树可见，该组合服务的所有状态都从M 0可达并且可以激发转移到终止状态M 8。该组合服务具有前进性。在可达树中，任意状态之间没有出现无意义的循环。由上述分析可知，该服务组合实例满足正确性要求。并且由定义3可知，该服务组合模型是合理的。5 结论Web 服务组合是Web 服务的一个重要研究方向。本文分析了形式化方法Petri 网的优势，结合Web 服务的定义，给出Web 服务组合的形式化定义并给出图形化表示，并给出Petri 网模型生成算法。采用了Petri 网技术对Web

30、组合进行描述，并对组合服务的可达性、安全性、有界性、活性、完整性和前进性等特性进行了验证分析并进行了实例分析。下一步的工作是分析复杂的服务组合任务及建立更加完善的模型工具。按前述Petri 网模型生成算法生成组合Petri 网组合模M i =(i , p 1, p 2, p 3, p 4, p 5, p 6, p 7, o 。M 0 t1M 1M 3t3M 4 M 58t6M 6 t7M 7t8M 8=(0,0,0,0,0,0,0,0,1图11 组合服务实例的可达树型，采用可达树生成算法构造可达树，如图11所示。参考文献：1 2廖军, 谭浩, 刘锦德. 基于Pi-演算的Web 服务组合的描述和验证J. 计算机学报, 2005, 28(4: 635-643.Wil van der Aalst. Pi Calculus Versus Petri Nets-Let us eat humble pie rather than further inflate the Pi hype DB/OL. 2005. http:/tmitwww.t