论文部分内容阅读
Workflow is a fast evolving technology which is being exploited by businesses and a variety of industries.Workflow modeling and verification(control-flow verification)are the first，and arguably the most important，steps towards taking full advantage of workflow technology.In[6]，Aalst argued that Petri net is suitable for modeling workflows.A special kind of Petri net for workfiow modeling，workflow net(WF-net)，was proposed and the 1-soundness/soundness properties were introduced as the correctness criteria for determining good WF-net models.The1-soundness property can be verified by the well-known algorithms for checkingthe liveness and boundedness of Petri net systems.Soundness is a much stronger requirement than 1-soundness and is also harder to be verified.
Addressing the above problems，in this thesis we：
(1) Solve he soundness problem effectively for some kinds of WF-nets by establishing the relationship between 1-soundness and soundness for them.In section 2，we prove that for several kinds of WF-nets-ST-Asymmetric choice WF-nets，Extended Free-choice WF-nets，Extended None Self-controlling WF-nets，Well-handled WF-nets，State-Machine-Allocatable WF-netstheir soundness can be implied by their 1-soundness.It is also proved that for Extended Free-choice WF-nets and Well-handled WF-nets which are widely used in most WfMS，their 1-soundness(and their soundness)can be verified in polynomial time.
(2)Propose a special kind of WF-nets，the Well-handled with Regular Iteration WF-nets (WRI WF-nets)which is inherently sound and powerful enough for many modeling problems.WRI WF-net is a special kind of WF．net that enforces the balance of“split”and“merge”structures.Moreover,only regular iterations are allowed in WRI WF-nets.With these restrictions，we prove that WRI WF-nets are inherently sound.This property would greatly reduce the verification efforts during workfiow modeling.WRI WF-nets are especially useful for modeling workflows with relatively simple control-fows，e.g.，the modeling of software processes.
(3)Based on NN-WF-net，introduce the NN-soundness property as its correctness criterion and examine the verification of NN．soundness.NN-WF-net is a multi-dimensional workflow model introduced in[26] and is very useful for workflowmodeling problems in cross-organizational environments and can improve the flexibility and the scalability Of workflow management.Based on NN-WF-net，we propose the NN-soundness property as its cOrrectness criterion and also solve the verification of NN-soundness by transforming a NN-WF-net to a WF-net with a set of translation rules.
(4)Use above results to guide the workflow verification in CPMS.CPMS is a process supporting system to help software companies improve the maturity level of their software processes.In the Process Definition Tool of CPMS in which thesoftware processes are modeled by dataflow diagrams，above results on workflow verification are used to guide the verification of control-flows of software processes.The dataflow diagram models are transformed tO the WF-nets to verify the 1-soundness and soundness property.A special tool is also developed in CPMS to support the process modeling with WRI WF-nets.