Research On Formalized Modeling And Simulation For Workflow Systems

Workflow is a computerized model responding to business processes, which can be executed by workflow management systems to support BPR (Business Process Reengineering) and BPA (Business Process Automation) in computer environment. With the development of computer technology, the research and application on workflow are receiving more and more attentions by academic circles and business community.Definition and simulation on workflow is a very complicated process and it is easy to make a mistake. So a workflow modeling method which is simple to be used in reasoning and verification is needed. In this way, it is necessary to establish a formal model during designing period. The character of the system can be validated and optimized through simulation and analysis on formal model.Although large numbers of modeling methods have been proposed by organizations and researchers, researches on simulation technology still need to be deeper. As a representation of process algebra, CCS (Calculus of Communicating System) has rigorous syntax and semantics. It can be used to reason and verify the properties of systems. In addition, its LTS (Labelled Transition Systems) semantics is used to describe the state transition process of the formal model. In this way, an equal automation model can be constructed to denote the executing trail of the formal model and check the semantical attribute for the system.CCS is considered as the theoretical basis of the whole research work. At first, a formal workflow model is established using a CCS-based language. This model can support a number of components working parallelly and cooperation in large-scale, complicated, distibuted system. Then the equal execution model which is used to check and anlyse the semantic character of formal model can be constructed, according to its LTS semantics. Details include the following steps.(1) A CCS-based formal model for workflow system is established. By analysing characteristic of workflow system and CCS model, we can match all the elements in workflows with those in CCS. Atomic activities in workflows are corresponding to the atomic processes in CCS, and tasks and sub-workflows including workflows themselves are corresponding to compound processes. The formal model built in this way can hold the syntax and semantics from CCS. Business processes executed by different operators and workflow productions output by different companies can be considered as sub-workflows of the systems. Then, interaction between them can be excellently depicted, by the interleaving semantics of the model. (2) The method of constructing execution model is introduced. The execution model, which is a finite Automation actually, describes the executing process of formal model. The constructing process is started from initial state. The set of Exposed Events under every state of systems can be canstructed by pursuing changes of process expression, and the mapping relationship among primary state, transition event and target state and the executing contrail of the formal model can be got. Then the automation model which describes the executing process of formal model can be constructed.(3) The semantic correctness of the execution model is proved. The content of this part is to prove the semantics of execution model and of the formal model are equal. Since the execution model is established by pursuing the changes in corresponding compound expression for formal model, semantic equivalence verification can be transformed into verification on consistent between changes in compound process according with formal model and in state transition described by exexution model. In this way, the semantic correctness of the execution model can be proved.(4) A simple example is used to explain how to establish a formal model for workflow system, how to construct the execution model which can be exported as a state transition graph, and how to anlyse the character of workflow systems according to the execution model. Through case study, it can be summarized that the execution model can be used to check some semantic characters of workflows, such as consistency between systems’ behaviours and exposed behaviours, their validity and security and so on.(5) The work is summarized in the last part and future works are pointed out. In fact, since theπ-calculus is evolved from CCS, the research work introduced in this paper can also supportπ-calculus.