摘要 : The correctness of workflow systems is dependent on not only their control-flows but also their data-flows. <italic>WFD-nets</italic> (Workflow net with data) can model both control-flow and data-flow of workflow systems, and are ... 展开 The correctness of workflow systems is dependent on not only their control-flows but also their data-flows. <italic>WFD-nets</italic> (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 expression <italic>w.r.t.</italic> data and can determine the progress of control-flow. In order to solve these problems, we propose a <italic>guard-driven reachability graph</italic> that 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. 收起