Model Checking of Workflow Nets with Tables and Constraints

Many operations in workflow systems are dependent on database tables. The classical workflow nets and their extensions (e.g., workflow nets with data) cannot model these operations, so that they cannot find some related errors. Recently, workflow nets with tables (WFT-nets) were proposed to remedy such a flaw. However, existing methods for constructing the reachability graph of the WFT-nets can generate pseudo states because they do not take into account the guards that constrain the enabling and firing of transitions. Additionally, only the soundness property of WFT-nets is considered that represents a single design requirement, while many other requirements, especially those related to tables, cannot be analyzed. In this article, we re-define the formalism of WFT-nets by augmenting the constraints of guards to them and re-name them as workflow nets with tables and constraints (WFTC-nets). We propose a new method to generate the state reachability graph (SRG) of WFTC-nets such that the SRG can avoid pseudo states by considering the guard constraints. To represent design requirements related to database operations, we define database-oriented computation tree logic (DCTL). We design the model checking algorithms of DCTL based on the SRG of WFTC-nets and develop a tool. Experiments on several public benchmarks show the usefulness of our methods.