A Guard-Driven Analysis Approach of Workflow Net with Data

Abstract

The correctness of workflow systems is dependent on not only their control-flows but also their data-flows.WFD-nets(Workflow net with data) can model both control-flow and data-flow of workflow systems, and are used to analyze/verify their correctness. The existing methods of analyzing/verifying WFD-nets are based on their reachability graphs. However, the reachability-graph-based methods have two flaws: state space explosion and pseudo states, since the guard functions are not handled perfectly. Note that every transition of a WFD-net is labeled by a guard function, which is a Boolean expressionw.r.t.data and can determine the progress of control-flow. In order to solve these problems, we propose aguard-driven reachability graphthat can both alleviate the state space explosion problem and avoid pseudo states. We describe the related algorithms and develop a tool. A group of experiments illustrate the advantage and effectiveness of our approach, and an example of property loan shows its usefulness.

Cite this work

No public copy is stored for this record, so only the metadata is cited.

Stored only when both papers are in the corpus — 19 citations exist upstream.

Papers that cite the same references — the relational fallback while embeddings are still backfilling.