Control-flow and data-flow modeling and verification are two important challenges for traditional workflow management. To formulate the data-flow modeling and verification, a Petri Net based approach is proposed in this paper. More specifically, the WFIO-net, which is a kind of WF-net by extending each activity with its read and write data sets, is first presented to model both the control-flow and data-flow information in a workflow process. Moreover, the firing rule of WFIO-net which is different from traditional Petri net is discussed in detail. Then the formal definitions of three basic types of data-flow errors, including missing data, redundant data and conflicting data are formulated using WFIO-net. Next, a polynomial complexity algorithm which is capable of detecting the above-mentioned three kinds of basic data-flow anomalies is proposed based on the activity-data incidence matrix of the WFIO-net. A running case of a property loan approval business process is given to validate the proposed method.