Modeling And Verification Of The Workflows Based On UML-Statecharts

Workflow is one of the technologies developed most rapidly in computer integrated manufacturing field recent years. At present, many productions have been applied to practice, for instance, Metero,WIDE, and so on. But majority of the productions lack for verification of correction or only check the local expressions during the modeling process, so causing the existence of the deadlock, livelock and other bugs in the model. It causes many problems directly during the dynamic execution of the workflow. So it is important that model and verify the workflow before running. Furthermore, it can reduce the cost of correcting the error greatly if we find errors existing in the process definition before the execution of the workflow.Modeling the control flow, temporal constraints and data flow of workflow based on UML Statecharts respectively, and then verifying the correctness of them by formal method is the main contribution in this paper. In addition, we also model and verify the concurrent workflow based on UML Statecharts.The workflow model is built by UML Statecharts in this paper, and the correctness of the control flow in workflow is verified, including the verification of soundness and the properties of semantic-related of the control flow. Verifying the soundness of the UML Statecharts model can be translated into the verification of the soundness of the global reachable state transition diagram, and the algorithms verifying the soundness and the properties of semantic-related are given.At the aspect of verifying the consistency of temporal constraints of workflow, the time events are added into the UML Statecharts, then the rules translating the extended UML Statecharts into timed automata are given.The upper constraints(the most time interval between two tasks), lower constraints(the least time interval between two tasks) and deadline constraints are defined by TCTL. The consistency of these constraints in build time, instantiation time and run-time are defined respectively. Last, the temporal constraints are verified by ALUR's model checking algorithm.This paper also verify the correctness of the data flow of the workflow. The data flow objects are added into the UML Statecharts, and the semantic of data flow is...