Workflow Nets With Tables and Their Soundness

Workflow nets and their extensions with data flows, e.g., workflow nets with data and colored workflow nets, can well model the business processes of workflow systems, and their soundness guarantees that systems have neither deadlock nor livelock. However, some design requirements related to the changes of data values within multiple business cases are not reflected by these models, and thus, some errors of the modeled systems cannot be detected by them. In this article, we propose workflow nets with tables (WFT-nets) to model workflow systems that are closely related to the database (i.e., different users, records, and attributes). We define the firing rule of WFT-nets via data refinements in order to avoid infinite states caused by unbounded data. We use first-order linear temporal logic to represent the design requirements of records and attributes' values and then define the soundness of WFT-nets. We construct an algorithm to verify soundness. A tool is developed, and a group of experiments are done to illustrate the effectiveness of our methods.