基于Petri网的Web服务组合流程的验证

1、基于Petri网的Web效劳组合流程的验证论文导读：过程验证器将组合效劳转换为对应的Petri网，并通过检查PN模型的活泼度来判断是否存在死锁详见第三节。Web效劳组合被看作是一个组合的过程，根据一定的控制结构连接一些原子过程。关键词：Web效劳，面向效劳的计算，效劳组合，Petri网1、序言近年来，面向效劳的计算SOC【1】已经成为分布式环境下如网格或对等网络解决集成异构应用问题的主要方法。SOC下的效劳作为软件实体被定义，研究主要集中在一个效劳如何与其它效劳协作完成某个应用任务上。因而效劳组合被作为面向效劳计算下构建应用的主要方式。Internet的异构和动态的特性要求基于Web的效劳能够

2、按要求实现效劳，即现有的效劳能够协同工作以满足用户的要求【2】。目前关于效劳组合的研究工程，包括HP实验室的eFlow【3】，加利福尼亚伯克利大学的Ninja【4】效劳组合，斯坦福大学的SWORD【5】，都只是典型的加强效劳编制，忽略了用户和效劳的上下文。另外，请求者也许会由于上述方法中的缺乏组合效劳的过程验证而得到无效的组合结果。因此，本文提出了一种基于Petri网组合效劳建模机制【6】，同时引入一种验证算法以验证效劳组合流程的正确性。2、过程验证器过程验证器的主要功能是验证中介注册代理生成的效劳执行队列是否可行，并检查队列中是否存在效劳之间的不兼容。定义1. 一个假定的事件是一条XML消息

3、产生的。如果Web效劳WS1要求输入事件消息X在输出事件消息Y之前，而Web效劳WS2要求输入事件消息Y在输出事件消息X之前，这样一个顺序关系将导致WS1和WS2之间的无效组合。这种现象称之为效劳组合的不兼容性。过程验证器将组合效劳转换为对应的Petri网，并通过检查PN模型的活泼度来判断是否存在死锁详见第三节。如果存在死锁，效劳执行层将用中介层返回的效劳列表中的可供选择的兼容效劳替换掉效劳A或效劳B或是AB都替换掉。如果当前列表中没有可替换的效劳，那么效劳执行层将向中介层请求新的效劳或报告失败。最后将验证执行方案发送给执行引擎。3、验证组合效劳流程过程验证器利用Petri网对组合效劳建模，并

4、基于模型的模拟观察效劳的行为属性，包括平安性，可达性，死锁及冗余。Petri网对于以下特征的信息处理系统是一种很强的建模和分析工具，如协同并发式、异步式、分布式、平行式、非确定式、随机式。3.1、用Petri对组合效劳建模定义2. Petri网是一个四元PNP，T，F，M0，其中Pp1，p2，pm是一组有限的位置；Tt1，t2， ，tn是一组有限的转换；F属于(PxT)(TxP)是一组有向弧；M0：P0，1，2，3，是一个初始标记。每一个标记代表着一个令牌的分配。如果M是一个标记，那么M(p)代表在位置pP处的令牌数。定义3. 一个效劳流网是一个六元 SFNP，T，F，M0，pi，p0，其中P

5、，T，F，M0是一个PN；pi 是关于-pi xPT(x，pi) F的输入位置； p0 是关于p0-xPT(p0，x) F的输出位置；如果通过添加从t*到T、(pi，t*)及(t*，pi)到F的转换，那么SFN*是强连通。定义4. 一个组合的效劳是一个四元的CSN，D，E，SFN，其中N是CS的名称，用来作为组合效劳的唯一标识；D是CS的描述，它概括了组合效劳提供的内容；E是组成CS的一组子效劳，可以是一个根本效劳也可以是一个组合的效劳；SFN是由Petri网描述的效劳流模型。Web效劳组合被看作是一个组合的过程，根据一定的控制结构连接一些原子过程。因此，以下pi位置将被分解成多个代表不同的效

6、劳过程的位置点。根据效劳的描述，分解将基于图1所示的不同的控制结构来执行。当所有的组合过程被分解后，CS建模也就完成了。模型可以用来进行死锁、无穷循环及冗余等错误的分析和模拟。图1 基于控制结构的Petri3.2、模型验证组合效劳的过程可以通过分析对应的Petri网模型以及各种可以被Petri网应用的分析方法包括可达树、状态方程、映射矩阵来检查。本文采用可达树来执行一个流程模型的验证，通过将构造可达树与合法性验证相结合来实现。可达树是用来描述所有从初始状态开始的可达状态。在可达树中，代表M0和它所有可达的后继节点中：M0代表树的根结点；叶子节点对应系统的最终状态；弧代表相关的转换。从根结点到一

7、个确定的节点的路径代表一个可执行的序列。符号代表某个节点位置处的有效令牌数为无穷。本文的方法是通过检查流程网的状态和某个位置节点的有效令牌数，来实现构造可达树过程中的CS模型的验证。算法1. 一个CS模型的验证算法输入： 由Petri网表示的CS模型输出：可达树T(PN)方法：步骤1：初始化T(PN)的根结点r，令MrM0；步骤2：x是一个叶子节点当且仅当以下条件满足：(a)Mx不存在激活的转换，例如， tTMx (t) ；(b) 从节点r到节点x的路径上存在一个节点y满足MyMx且yx。如果所有节点中除了节点r之外都是叶子节点，那么转到步骤7，否那么转到步骤3；步骤3：如果x不是叶子节点，那

8、么在Mx处至少存在一个激活的转换。触发所有激活的转换tT，以生成一组子节点 Mx (t)Mx (t)是由触发所有可激活的转换t根据x的输出定位的产生的标注；t是从节点x到Mx (t)的弧，令y表示新节点；步骤4：计算标注Mr。首先计算序列Mx的子序列M，利用公式 pP, M(p)= Mx (p)-W(p,t)+W(t,p),然后计算My：如果从节点r到节点y的路径上存在节点z满足M(p)Mz (p)且zy，那么My (p)=M(p), M(p)= Mz (p); 否那么 My(p) =M(p)。步骤5：检查每个位置的有效令牌数。如果满足 pPMy(p)1，那么流程结构是平安的，转到步骤2，否那

9、么转到步骤7；步骤6：假设Lset是可达树中的一组叶子节点，Mg是用户目标的标注。验证模型的正确性步骤如下：(a)流程模型是可达的，当且仅当 $T*M0()Mg，代表有效转换中的依次转换序列；(b)流程模型是有效的，当且仅当 $MiLsetMi (p) 且 Mx(p), My(p) Lset, 满足Mx(t) My且My(t) Mx ；Mi (p)0,pp0 。步骤7：结束。4、总结及以后的工作本文提出的一种基于Petri网对组合效劳进行建模，并采用可达树来验证组合效劳的正确性算法，保证了组合效劳的平滑执行。今后的研究工作将落在运行时组合效劳的修改流程的验证问题上。例如，由于符合过重或是运行效劳的主机不在线等原因，导致的执行某项特定任务的组合效劳中的某个已选择的子效劳失效了，此时系统那么需要根据新的上下文自动调整，替换或移除该子效劳，并通过过程验证器动态地验证调整后的流程。参考文献：【1】喻坚,韩燕波.面向效劳的计算原理和应用.清华大学出版社 ,2006,pp.112-248.【5】 Shankar R. Ponnekanti, Armando Fox, SWORD: A Developer Toolkitfor Web Ser