Study Of Service-Oriented Business Process Modeling And Verification

A business process describes the abstraction and view of various managementlogics inside and across organizations. In the area of Business Process Management(BPM), Service Oriented Architecture (SOA) provides a series of technicalspecifications for establishing business processes across organizations. Business processmodeling, as an essential part of BPM, is the beginning of the whole life cycle of abusiness process. Process model verification is a technique of checking the correctnessof process models, which plays an importance role before a process runs into operation.A process model is usually designed with graphic languages, while BusinessProcess Executable Language (BPEL) is the de facto standard of the process definitionand execution language in BPM and SOA. The control flow structures of BPEL aremainly block-oriented, which complicates the transformation of graphic process modelsinto BPEL. Workflow net (WF-net) is a kind of process models based on formal theories.It has been widely accepted by the academic community. Reduction technique is animportant method of process model verification. It alleviates the state explosionproblem, and facilitates the automation of verification. However, for a prominent classof formal process models called free choice WF-net, a specific reduction method isabsent.The contents of this dissertion fall into two parts: first, a method of businessprocess modeling based on model transformation is proposed. The graphic UnifiedModeling Language (UML) is used to design process models, the formal process model,WF-net is utilized as theory foundations, and a BPEL process definition is taken as thedestination model. Secondly, a sound and complete reduction rule set for free choiceWF-net is presented. It provides a specific reduction technique for the verification ofthis kind of process models. Then their synthesis rule set is given, which provides ameans to analyze the control flow structures of graphic process models.The contributions of this dissertation are as follows:1. The information on the resource and data aspects of business processes isrespectively modeled with UML composite structure diagrams and class diagrams. Themapping rules from composite structure diagrams to BPEL process partners, and rulesfrom class diagrams to data definitions of BPEL are separately defined. This methodconsiders the information beyond the control flow dimension of business processmodels, and improves the generation of BPEL from UML process design models.2. A transformation of UML activity diagrams into BPEL control flow models is presented, in which WF-nets function as intermediary models. First, an activity diagramis mapped to a free choice WF-net. Then this net is transformed into a separable WF-net,from which a BPEL control flow model is generated. Compared with the direct mappingfrom the source to destination model, this method has reliable theory foundations andequivalence proof.3. Two formal methods are proposed for the transformation of free choice WF-netsinto separable WF-nets. In the first one, the formation of overlapped patterns (OP) in thecontrol flow structures of graphic process models is analyzed. Then the existing meansto handle OP is formally described, and its application range is summarized.Furthermore, the trace equivalence of transformation is proved. The second methodprovides a partial net unfolding algorithm for acyclic free choice WF-nets to obtain theirseparable forms under the notion of true concurrency equivalence. In addition, thesufficient conditions that two safe nets are true concurrency equivalent are described.4. A sound and complete reduction rule set is presented for free choice WF-nets.The soundness determines that the behavioral correctness of such a model is preservedduring the reduction, and the completeness ensures that every such a correct WF-net canbe finally reduced to its simplest form. A reduction technique with more specificapplication range is provided for process models.5. A sound and complete synthesis rule set is given for free choice WF-nets. Thenthe rule set is restricted to preserve the separability of separable WF-nets. For the twoclasses of WF-nets, this method provides their modeling with fine-grained guidelines ofa different dimension compared with the node refinement.