Many operations in workflow systems are dependent on database tables. The classical workflow net and its extensions (e.g., worflow net with data) cannot model these operations so that some related errors cannot be found by them. Recently, workflow nets with tables (WFT-nets) were proposed to remedy such a flaw. However, when the reachability graph of a WFT-net is constructed by their method, some pseudo states are possibly generated since it does not consider the guards that constrain the enabling and firing of transitions. Additionally, they only considered the soundness property that just represents a single design requirement, so that many other requirements, especially those related to tables, cannot be analyzed. In this paper, therefore, we re-define the WFT-net by augmenting constraints of guards to it and re-name it as workflow net with tables and constraints (WFTC-net). We propose a new method to generate the state reachability graphs (SRG) of WFTC-nets such that SRG can avoid pseudo states, due to the consideration of the guards in it. To represent design requirements related to database operations, we define database-oriented computation tree logic (DCTL), to represent more design requirements. We design the model checking algorithms of DCTL based on the SRG of WFTC-nets and develop a tool. Experiments on a number of public benchmarks show the usefulness of our methods.

翻译：工作流系统中的许多操作依赖于数据库表。经典工作流网及其扩展（如带数据的工作流网）无法对这些操作进行建模，因此无法发现相关错误。近期，研究者提出带有工作表的工作流网（WFT-net）以弥补这一缺陷。然而，当采用其方法构建WFT-net的可达图时，由于未考虑约束变迁使能与触发的守卫条件，可能生成伪状态。此外，现有研究仅关注表征单一设计需求的正确性属性，导致许多其他需求（尤其是与工作表相关的需求）无法被分析。为此，本文重新定义WFT-net，通过增加守卫约束扩展模型，并将其重新命名为带约束和工作表的工作流网（WFTC-net）。我们提出一种生成WFTC-net状态可达图（SRG）的新方法，该方法在构建过程中考虑守卫条件，使SRG能够避免伪状态。为表征与数据库操作相关的设计需求，我们定义了面向数据库的计算树逻辑（DCTL），以表达更多设计需求。基于WFTC-net的SRG，我们设计了DCTL的模型检测算法并开发了相应工具。在多个公开基准测试上的实验结果表明了本文方法的有效性。