Research For Formalizing Workflow Model

Workflow technique is widely used in many application fields. Workflow modeling technique is always one of important research tasks of workflow, including workflow model definition and semantic formalized expression method etc. To realize the function of workflow management, the business process must be abstracted from the real world and described by a kind of modeling method. The result is workflow model. According to the analysis of domestic and international research on workflow modeling technique, workflow model is short of a kind of formal mathematics model to support process definition and process analysis. Point to these defects, the thesis mainly studies a method for constructing a workflow model and analyzing method of workflow model based on theπ-calculus.Theπ-calculus is a kind of mobile process algebra which can be used to model concurrent and dynamic systems. Had campared and analyzed most of modeling tools, a method of workflow modeling based on theπ-calculus is proposed. The method sets forth expression of all kinds of activity and dependency in using theπ-calculus and introduced a formal semantics for workflow patterns, which is based on theπ-calculus. All patterns have been formalized with concise and unambiguous expressions. The behavior of each workflow pattern has been defined precisely. The method is complete formalizations, and it has a strong capability of semantics express. The formalizations can be used as a foundation for workflow execution, reasoning, and simulation. It has been proved that the approach can describe clearly and accurately the process of practical application and is an effective method to set up a workflow model.The effective process verification in modeling phase is very essential. This thesis studies the analysis of workflow model based on theπ-calculus and validates correctness of workflow in using theπ-calculus. For validating semantics, a solution based on lazy soundness was proposed. This thesis utilizes theπ-calculus to discuss and implement reasoning on lazy soundness.