Computing and Informatics

The existing modeling methods for business process management systems (BPMS) focus on the logical and abstract data layers but often ignore operations related to the underlying database, thus failing to describe system behavior accurately. Workflow nets with tables (WFT-nets) compensate for the lack of description of database table operations in existing modeling methods. However, for timed business process management systems (TBPMS), their correct behavior depends on the logical correctness of the results obtained by the operational process and the time required for each activity to be correctly executed within a specified time. Since WFT-nets do not consider time properties, they are unable to describe time-related activities in TBPMS, potentially leading to incorrect results. This paper introduces timed workflow nets with tables (TWFT-nets), which add time elements to transitions to simulate time-constrained activities in the system. Additionally, we assign different labels to represent the execution strategies of activities under different time constraints. To analyze the soundness of TWFT-nets, we propose a timed database computation tree logic (TDCTL) model checking method and define soundness from three perspectives: logic control layer, data design requirements, and time constraints. We transform soundness into TDCTL formulas, provide a model checking algorithm, and develop a tool. Experiments show the effectiveness of our methods.