工作流过程的结构变化分析_英文_

14 t15 t13 t12 1314 121011 X ( X ? P ? T ), PN |= (P ? X ,T ? X ; F ? ( X × X X )) . WF1 (iv) For every N k TN= N; kkp p p pt3 t4 t9 8t10 3 42 //TNis a temporal node set of Nbefore extension. k k p p p t5 t2 1 7 9 Repeat pp p pt11 t8 t7t6 5 6 1615 o t17 p := φ, p:= φ ;t1 Temp=N; i kik ok • • ppt14 17 18 Pr e = { p | p? ? φ ?p ? N = k k pt12 pppt16 t17 t13 1014 1112Nφ} ; //Previous neighbor places of nodes in N. k t15 pp• • 20 19 Post = { p|p ? N ? φ ? p? N = k k WF2 φ} ; ? If ?p? Pr e : ?p ? N , there exists a path 1 k Fig.4. Workflow Net with two Change Regions frompto p, then p:= p; 1 ik 1 //pis a temporal source place. ik At first, N is initialized as {t,t,t,t,t,t, t,t}, 256814151617•• ?there exists a path If ?p? Post : ?p ? N then N := N ?N ? N . Subsequently, it is 2 partitioned ,from p to p, then p:= p; 2 k ok 2 to three parts N, Nand N. For Nand N, the 12 31 2//pis a temporal sink place. ok extension are graphically shown in Fig.5. During the • For every p ? N\ { p} , N:= N ? k ik k k iteration, these two parts are merged. Finally, two • For every p ;p ? N \ { p} , N:= N? k ok k k change regions are generated and indicated within the •For every p ;t ? N , N:= N ? t ? k k k • 4 //Nis extended to its adjacent transitions and places;t ; k Let PN = (P , T ; F ) , PN = (P ,T ; F ) , and 1 1 1 1 2 2 2 2 If ?l ?{1,..., m}, l ? k : N ? N? φ, then k l P? P,T? T, F? F, set PN= PN? PN= (P,T; F) , such 2 1 2 1 2 1 3 1 2 3 3 3 mergethat Nand Nas N := N ? N , break;P= P? P,T= T? T, F= ((P× T) ? (T× P)) ? F. k l kl k l 3 1 2 3 1 2 3 3 3 3 3 1 第 20 卷第 7 期 Vol. 20 No. 7 2008 年 4 月系统仿真 学 报Apr., 2008 α = p α dotted rectangles in Fig.4. and α= pαp, then the path via t 5 251 ok p4 ik 41 1 α = p α p tp α is C ppp . 2 46 ik 41 1 2 51 ok Lemma 2. Every old change region WF is also 1k p t5 t2p 17 a (or an informal) workflow net. pp pp t8 t6 16 515 6 Informal workflow net is a connected set of N 1 N 2 nodes with multiple source and sink places. It can be (a) Nand Nare initialized 1 2 considered as an extension of standard workflow net. The proof of this lemma is straightforward according Pre={p}, Post={p,p} 11125 2 to the definition and Lemma1. pp3 t3 p=p, p= φ i11o1 p1 Theorem 1. Let WFbe a sound workflow net, t2 1 N:= N? {t, t, p, p} 1 1 3 7 3 6 WFbe the new workflow net after structural change, p5 p6 p15 t6 t72 C (WF,i) is safe and sound iff ?k : (WF, p) is safe(b) Nis extended 2 1 2 k ik and sound. Proof. The change procedure is a substitution the p2 p3 p4 t3 old region by the new region, in terms of the p1 t5 t2 p7 Petri-net-based model, the change can be considered p15 p5 p6 t6 p16t7t8 C C as the replacement of subnets WF by WF in WF , 1 1k 2 k which results in WF. Such a modification can be 2(c) Nand Nare merged as N 1 2 12 further considered as a combination of transition abstraction and refinement. On the one hand, the Pre={p}, Post={p} p2 p3 t4 p4 1117t3 C behavior of each WFcorrespondsto a single 1k p=p, p=p. p1 t5 i11o27t2 p7 + + transition t . On the other hand, the transition t k k N:= N? {t } 12 12 4 p15 p5 p6 p16 t6 t7 t8 C can be refined by the subnet WF . As a result, the 2 k (d) Nis extended 12 conclusion can be drawn. With respect to refinement Fig.5 Change Region Generation and abstraction, a detailed discuss is presented in [15]. Theorem 2. Let WFbe a sound workflow net, 1 3.2 Approach to Check Feasibility based on WFbe the new workflow net after structural changes, 2 Change Region C C Be(WF) = Be(WF) iff ?k : Be(WF) = Be(WF) . 1 2 1k 2 k C C In the following, we will prove that the change Proof. t ...t ,t ? ?σ? L(WF) , σ ... ... 1 1ki l k 1 1 1 1 1 C C C C region calculated by the algorithm can be used to = t) ?Twhere t,..., t?T\ (and t,..., t?T. It is k 1k1 l 1 1k1 1ki 1k validate the feasibility of structural changes. C C CC C obvious that for all k: σ = t t... ( ). As t? L WF 1k 1k1 1k 21ki 1k CLemma 1. Every new change region WF is a 2 k C C the behavior of WF is united with WF , therefore 1k 2 k workflow net. C C C C = Γ?σ ? L(WF ) : (σ(σ , it C C C C C C 2 T ?T ?T T ?T ?T Proof. Firstly, we prove there is at least one 1k 1k 2 k 2 k 1k 2 k Γ2 k 2 k C C C ))source place p. At worst, the new change region is the1k k σ = t t ...t . Nowmight as well to assume ik2 k 2 k1 2 k 2 2 kj CC C whole net, that is to say, the algorithm will always considering sequence σ = t...t...t...t, such 2 1 2 k1 2 kj l terminate. In such situation, pis just the source place ik C that(σ ) = t t. ..t . and (σ ) = σ C Γ 2 1 2 lT?T\( ?T) C 2 2 k 2 2 k T ?T 2 2 k of WF. Similarly, there is at least one sink place p. 2okΓ 2 k Intuitively, σ is obtained from σby 2 1 Secondly, we prove that the source place pis a ik replacing singleton. According to the algorithm, Nis updated k • those transitions within the change regions by for ?p ? N \ { p} , N := N ? p . Hence there k ik k k corresponding modified transition sequences, while only one source place. Similarly, the sink place pis ais ok keeping the remnant sub-string untouched. It is clear singleton. Γ (L(WF )) ? Γ ( L(WF )) .that Γ(σ) = Γ(σ ) and σ ? Thirdly, we prove the connectivity. For ?p ? N , T ?? 1 T ?? 2T ?? 1 T ?? 2 2 k 1 2 2 there exists a path α(α ) from p(p) to p(p), ikok1 2 L(WF) , thus Similarly, Γ(L(WF)) ? Γ2 1 2T ?? 2 T ?? where (L(WF)) . Therefore, Γ(L(W1 F)) = Γ(L(WF)) , 2 1 T ?? 1 T ?? 2 α = p α p α = pα p , then p is on the 1 2 Be(WF) = Be(WF) .andpathi.e., 1 2 1 ik 112 21 ok C • • from source to sink. For ?t ? N ,α = p α pα ( ? k = 1 : For ?σ ? L WF , ?σ ? ) k 1 1 1 1k supposing p ?and p ? t . Since there is 1 2 C pC C L(WF )3 ik 11 21 ok satisfying σ = σ σ tawhere σ(σ) ? T= path α (α) fromp(p) to p(p), such that11 12 1k ik21ok 4 5 σ ,1 11 1k 12 φ . As Be(WF) = Be(WF) , that is to say, ?σ ? N ' is formed, and N '? P'?T temporal nodes set 1 2 2 k k C ' . L(WF) ,Therefore, p(? i') is selected as a temporal sourceΓ (σ ) = Γ (σ ) . If we set σ = σ σ σ , 2 1 k 1 2 thenC C T ?? 1 T ?? 2 2 11 2 12place for further extension. In fact, if i' is selected as (σ ) =it is apparent that σ ? L(WF) . Since T?? 12 k 2 k 1 a source place, WF ' will be generated finally. That is C C Γ ( ( (Γ σ Γ σ Γ σ = σ σ, ))) ) C C C ( T?? T?? T?? 11 1k 12 111k 121 1 1 T?T?T 1k 1k 2 k to say, there is a directed path from p to i' , hence it is 1 Γ σ on the other hand Γ (σ ) = σ Γ C C 2 11 12T ?? 2 k T?T?T2 2 k 1k 1k unreachable from to pfor loop-free structure.i' 1 C C C (σ )σ ,C accordingly Γ (σ) = Γ (σ ) . As C C C C C 1k 2 k T?T?TT?T?TThus, i' can’t be the source place of WF ' . As a 1k 1k 2 k2 k 1k 2 kC aC C result, Γ ( L(WF)) ? Γ ( L(WFconsequence, WF ' is not a legal and minimal change C C C C C C 1 T ?T ?T T ?T ?T 2 1k 1k 2 k 2 k 1k 2 k )) .region, which contradicts to the assumption. k It can be proven in the same way that C C The situation is complicated for loop structure. Γ (L (W F)) ? Γ C C C C C C 2 k 1k T?T?TT?T?T 2 k 1k 2 k 1k 1k 2 kThe generated change region may not be the minimal C C ( L(WF )) . Therefore, Be(WF) = Be(WF) . 1k 2 k one. Therefore, we should improve the algorithm so as It can be analyzed for the situations k > 1of to be suitable to loop structure. using inductive reasoning. Given a workflow net WF = (P,T ; F ) , if there Theorem 3. Let WFbe a sound workflow net, 1 exists a loop with being the entry point and pp i0ijWFbe the new workflow net after structural changes, 2 being the exit point, as shown in Fig.6, two subnets Be(WF) < Be(WF) iff: 1 2can be derived by excluding loop from WF. C C (i) ?k : Be(WF ) < Be(WF ) ; 1k 2 k C C ,B (ii) ?i : i ? k Be(WF ) = Be(WF ) or 1i 2 i ……C C Be(WF) < Be(WF) .tkm t k1 1i 2i The proof of this theorem is similar to the above WF …… tk0 ti0 pi0 pij ti1 tij proof and is omitted. A The above theorems indicate that the structural …… ……1 ELWF correctness and behavioral consistency of change pij' tkm pi0 pij tk0 ti0 ti1 tij tk1 A B regions imply the feasibility of change. Since the changes have no impact on the activities outside the ………… 2 ELWF p tk0 ij pi0' pi0 ti1 tij ti0 tk1 tkm change region, then it is sufficient to analyze the A B change region instead of the whole workflow model. Fig.6 Excluding Loop net The example shown in Fig.4 is appropriate to ELWF=(P,T; F), where 111demonstrate the usability of this approach. There are P= P ?{ p'} ;C C C C 1 ij WF /WF and WF /WF . It is two change regions 11 21 12 22 C C F= F \ {(t, p), ( p,t)} ? {(t, p'),( p',t)} . 1 km i 0 ij k 0 km ij ij k 0 easy to prove that Be(WF) < Be(WF) . Nevertheless, 12 22 ELWF=(P,T;F) , whereC 222the behavior of WF is contradicted to the behavior 11 C P= P ? { p'} ;C 2 i 0 L(WF ) = t t t t + t t tWF , since while of 21 11 2 3 4 5 6 7 8 C F= F \ {(t, p), ( p, t)} ?{(t, p' ), ( p', t)} . 2 i 0 i 0 ij k1 i 0 i 0 i 0 k 1 above L(WF) = t(tt+ ttt)t. According to the 21 2 34 6 7 8 5 ELWF(i=1,2) is called the excluding loop net that itheorems, the structural change is improper. is derived from WF. 3.3 Algorithm Improvement for Loop The algorithm in Section 3.1 is modified in the * Structure site to tackle workflow net with loop structure. There should exist a path from p(p) to p(p) in every net 12Theorem 4: For loop-free workflow process, the from R(WF), when locating pand p. For loop-free C C C C 2ik okchange region WF= (P,T; F) is a minimal one, 2 k 2 k 2 k 2 k structure, R(WF)={WF}; otherwise, R(WF) is the 222i.e., it does not cover other subnet WF ' = (P',T '; F ') , C C set of all excluding loop nets derived from WF. It is 2such that WF ' contains TN andP'? P,T '? T k 2 k 2 easy to prove that the generated change region by the C ,F '? F. k 2 k improved algorithm is a minimal one. C Proof: Supposing WF (with source place p) is ik2 k Note that, the excluding loop net does not destroy not a minimal one, then a legal and minimal subnet the connectivity. For any nodes x and y, it is reachable WF ' = (P',T '; F ') exists with the source place i' . Thus from x to y in WF iff there exists a path from x to y in there is a directed path from pto i' , and not vice ik ELWFor ELWF. Therefore, the preceding theorems 1 2versa. The algorithm is executed by adding new are also tenable for the improved algorithm. adjacent nodes. During the repetition procedure, a 第 20 卷第 7 期 Vol. 20 No. 7 2008 年 4 月系 统 仿真 学 报Apr., 2008 At the same time, a public survey is carried on. After 3.4 Discussion that, both the specialist and public opinion are The verification of feasibility consists of two reported to the leadership, who will review and phases. Firstly, to generate the change regions. approve or reject the application. Relevant documents Secondly, to check the structural correctness and will be issued and declared for those approved behavioral consistency of change regions. For application. And the approval result will be notified to arbitrary WF-nets, the problem of reachability is the applicant. Finally, the process terminates after EXPSPACE-hard. While the change region generation archiving is performed. The procedure is described as is polynomial complexity, so there is no increase in a workflow net WFin Fig.7, and the meanings of 1 computing complexity of this two-step procedure. transitions are explained in Table1. In practice, a workflow process may have thousands of activities, while the structural change is t6p3 t3 relatively minor. Therefore, from a practical point of p4 p5 t8 p6 t9 p7view, this approach is acceptable and efficient. t7 p14 t15 t16 p1 p12 t14 p13p15 p16 t2 p2t4 t13 t18 t19 t1 i Experiment result shows that the improvement in t17 p8 p10 t10 p9 t11 o terms of time and space is satisfying for large and t5 p11 t12 complex systems. WF1 How to check the soundness and behavioral p3 t6 consistency of change regions is out of the scope of t3 p17 p5this paper. Fortunately, various analysis techniques t7 p18 p6 t20 t8 t9 p7and tools for Petri net have been developed. Therefore, p 4 p14 t15 t16 p19 p1 p2t21 p20 p12 p13t1 t2 4 t13 t14 tthe change feasibility problem is decided and checked p15 p16 i t18 t19 t17 p8 p9 t11 p10 t10 o effectively for practical workflow processes. p11 t5 t12 It should be made clear that the change feasibility WF2 condition differs from the instance migration condition. The latter focus on the problem of under which Fig.7. Examination & Approval Procedure condition workflow instances can migrate from one Table1 Transition Explanation process definition to another. The change feasibility is t : receive material t : check 1 2 just one minimal requirement for workflow instance t: material incomplete : check OK t34 migration. Note that the change region can be used to t: check NOK t: supply material 56 t: technically examine t: financially examine 78provide a sufficient condition for instance migration, t: discuss t: survey 910i.e., any active workflow instance not marking the t: collect result t: cancel 1112places within the change region can be transferred to t: review t: report 1413the new workflow process safely. t : approve t : issue 15 16 t: reject t: notify 1718Case Study 4 t: archive t: classify 1920 t: legally examine 21Limited to the scope of paper, we give a simple example to illustrate the workflow process analysis In order to improve efficiency and for some responding to structural change. special needs, modifications are potential to be This is an examination and approval procedure. implemented. Firstly, the application material should The process starts when an application material is be classified before further examination. Another is to received. The first step is to check whether the parallelize the activities of technical examination and applicant the submitted has the qualification and financial examination. The last modification is that the If not, the material meets certain conditions. application is supposed to be examined not to violate case of application should be canceled. In any law or regulation. The new workflow net WFis 2 incompletion, the applicant is asked to supply material. formulated in Fig.7. These changes correspond to the Then responsible departments will investigate the addition of transition t, parallization of tand t, and 208 9items of application, and judge whether it is inserting of a new parallel branch t. 21economically or technically feasible. Based on the According to the algorithm, we can generate the examination, some specialists are gathered to discuss. C C change regions WF and WF , which are circled our ideas can be implemented and validated. 1 2 within the dotted rectangle. The change region is much Reference: smaller compared with the whole workflow net. The WfMC TC00-1003. Workflow Management Coalition. The Workflow [1] C number of reachable states of WF and WFis 10 2 2 Reference Model [S]. 1994. and 40, respectively. It is easier to validate the Stefanie Rinderle, Manfred Reichert, Peter Dadam. Correctness [2] C Criteria for Dynamic Changes in Workflow Systems-A Survey [J]. of WF . safeness and soundness In addition, 2 C C Data and Knowledge Engineering (S0169-023X), 2004, 50(1): 9-34. According to Theorem 2, the Be(WF) = Be(WF) . 1 2 CUI Li-zhen, ZHANG Shi-dong, ZHENG Yong-qing, et al. A Method [3] behavior of WFis united with WF, that is to say, the 1 2of Workflow Dynamic Modification [J]. Journal of System Simulation, potential changes are acceptable and the new 2003, 15(2): 264-266. workflow model WFpreserves not only structural but 2 FU Qian, ZHNG shen-sheng, DAI Kai-yu. Study on Workflow [4] also behavioral properties of the old process Simulation for Process Improvement [J]. Journal of System Simulation, 2003, 14(10): 1321-1324. definition. W M P van der Aalst. Inheritance of Workflows: an Approach to [5] Conclusion 5 Tackling Problems Related to Change [J]. Theoretical Computer Science (S0304-3975), 2002, 270(1/2): 125-203. When adjusting a workflow process to some Mathias Weske. Formal Foundation and Conceptual Design of [6] dynamic changes, it is critical to check the correctness Dynamic Adaptations in a Workflow Management System [C]// Proc. and consistency of the changes, so as to assures the of the 34th Hawaii Int. Conference on System Sciences, Jan 2001. Maui, Hawaii: IEEE Computer Society, 2001: 390-399. new workflow remains correct. This paper provides a C Ellis, K Keddara. A Workflow Change is a Workflow [C]// Business [7] pragmatic approach to tackle the process structural Process Management, LNCS 1806, 2000. W van der Aalst, et al. (Eds.), change problem. In this paper, we present a criterion S Berlin Heidelberg: pringer-Verlag, 2000: 516-534. to decide whether a structural change to workflow C Ellis, K Keddara, G Rozenberg. Dynamic Change within Workflow [8] process is feasible, i.e., no errors or inconsistencies is System [C]// Proc. of Int. ACM Conference COOCS’95, Milpitas, CA. introduced. Then we put forward an algorithm to USA: ACM, August 1995: 10-21. S Sadiq, O Marjanovic, M Orlowska. Managing Change and Time in [9] calculate the minimal region affected by the changes, Dynamic Workflow Processes [J]. International Journal of Cooperative which provides a better possibility to check the Information Systems (S0218-8430), 2000, 9(1/2): 93-116. feasibility for structural change. Furthermore, we S Rinderle, M Reichert, P Dadam. Flexible Support of Team Processes [10] discuss the workflow process with loop structure in by Adaptive Workflow System [J]. Distributed and Parallel Databases detail. This approach is applicable and efficient in (S0926-8782), 2004, 16(1): 91-116. terms of time and space for large-scale and complex W M P van der Aalst. Exterminating the Dynamic Change Bug-A [11] Concrete Approach to Support Workflow Change [J]. Information systems. Systems Frontiers (S1387-3326), 2001, 3(3): 297-317. The main result of this paper is significant both M Reichert, P Dadam. ADEPTflex: Supporting Dynamic Changes of [12] from a theoretical and a practical perspective. By Workflow without Losing Control [J]. Journal of Intelligent offering formal foundation for checking compliance of Information Systems (S0925-9902), 1998, 10(2): 93-129. workflow model, it provides concrete solutions for TADAO MURATA. Petri Nets: Properties, Analysis and Applications [13] problems today’s workflow management systems are [C]// Proceedings of the IEEE. USA: IEEE, 1989, 77(4): 541-580. JIANG Changjun, WANG Huaiqing, LIAO Shaoyi. Behavior [14] faced with. Relativity of Petri Nets [J]. Journal of Computer Science & The work presented here is a starting point and Technology (S1000-9000), 2002, 17(6): 770-780. there are numerous possible extensions. In theory, we W M P van der Aalst. Workflow Verification: Finding Control-Flow [15] intend to extend the dynamic changes to the data and Errors Using Petri-Net-Based Techniques [C]// Business Process the resource perspectives. In practice, we are currently Management. Germany: Spinger-Verlag, 2000: 161-183. in the process of building a prototype system where