| 算法1. 一个CS模型的验证算法
输入： 由Petri网表示的CS模型
输出：可达树T(PN)
方法：
步骤1：初始化T(PN)的根结点r，令Mr＝M0；
步骤2：x是一个叶子节点当且仅当下列条件满足：
(a)Mx不存在激活的转换，例如，' t∈T→┐Mx (t) ；
(b) 从节点r到节点x的路径上存在一个节点y满足My＝Mx且y≠x。
如果所有节点中除了节点r之外都是叶子节点，则转到步骤7，否则转到步骤3；
步骤3：如果x不是叶子节点，则在Mx处至少存在一个激活的转换。触发所有激活的转换t∈T，以生成一组子节点{ Mx (t)∣Mx (t)是由触发所有可激活的转换t（根据x的输出定位的）产生的标注；t是从节点x到Mx (t)的弧}，令y表示新节点；
步骤4：计算标注Mr。首先计算序列Mx的子序列M'，利用公式
' p∈P, M'(p)= Mx (p)-W(p,t)+W(t,p),然后计算My：如果从节点r到节点y的路径上存在节点z满足M'(p)≥Mz (p)且z≠y，则
My (p)=M'(p), M'(p)= Mz (p); 否则 My(p) =M'(p)。
步骤5：检查每个位置的有效令牌数。如果满足' p∈P→┐My(p)≤1，则流程结构是安全的，转到步骤2，否则转到步骤7；
步骤6：假设Lset是可达树中的一组叶子节点，Mg是用户目标的标注。验证模型的正确性步骤如下：
(a)流程模型是可达的，当且仅当 $б∈T*→M0(б)>Mg，б代表有效转换中的依次转换序列；
(b)流程模型是有效的，当且仅当 $Mi∈Lset→Mi (p) ≠ω且
' Mx(p), My(p) ∈Lset, 满足Mx(t)> My且My(t)> Mx ；
Mi (p)>0,p≠p0 。
步骤7：结束。
4、总结及以后的工作
本文提出的一种基于Petri网对组合服务进行建模，并采用可达树来验证组合服务的正确性算法，保证了组合服务的平滑执行。
今后的研究工作将落在运行时组合服务的修改流程的验证问题上。例如，由于符合过重或是运行服务的主机不在线等原因，导致的执行某项特定任务的组合服务中的某个已选择的子服务失效了，此时系统则需要根据新的上下文自动调整，替换或移除该子服务，并通过过程验证器动态地验证调整后的流程。
参考文献：
[1]喻坚,韩燕波.面向服务的计算－原理和应用[M].清华大学出版社 ,2006,pp.112-248.
[2]李景霞,侯紫峰.Web服务组合综述[J].计算机应用研究,2005年第12期,pp4-7.
[4] UC Berkeley Computer Science Division,The Ninja Project Overview, http://ninja.cs.berkeley.edu/, 2009-1-9.[EB/OL]
[5] Shankar R. Ponnekanti, Armando Fox, SWORD: A Developer Toolkitfor Web Service Composition, Proceedings of the 11thInternational World Wide Web Conference (WWW2002). Hawaii, USA, 2002,http://www2002.org/CDROM/alternate/786/index.html,2009-1-9.[EB/OL]
[6] 钱柱中,陆桑璐,谢立.基于Petri网的Web服务自动组合研究[J].计算机学报,2006年第7期,1057-1068.
2/2 首页 上一页 1 2 |
