Locating and Controlling Unsound Transitions in Workflow Systems Based on Workflow Net With Data Constraints

Data has a great influence on the analysis of the correctness of workflow systems. How to ensure that a system runs without data errors is very important. Workflow nets with data constraints (WFDC-nets) are a kind formal model that is good at specifying data oriented functional requirements in workflow systems. A sound WFDC-net can guarantee that the system is not only functionally correct but also meets all data requirements. Methods and tools for the soundness verification of WFDC-nets have been designed. However, how to locate unsound transitions in a WFDC-net and then effectively control them is still an open topic. This paper attempts to solve the issue and gives methods to optimize unsound workflow systems in design stage. In our solution, we first construct a minimal complete configuration tree based on the configuration graph with data constraints (C-graph) of the WFDC-net, and then we define four kinds of paths and algorithms to characterize unsound transitions. Furthermore, a pseudo intermediate set is constructed according to different paths and unsound transitions. Based on it, a 4-step controlling strategy is taken to optimize the system and finally makes the controlled system satisfy the data requirements. An e-commerce system is used to illustrate the feasibility and effectiveness of the proposed methods.