Detection of Dataflow Modeling Anomalies in Workflow Systems : Toward an Active Help Verification Using Model Checking

Business process modeling is a standard activity in the new technology of many organizations. Any information system needs to exchange data between activities by transit inputs and outputs. Workflow-net with data (WFD-net) has been used to verify the data anomalies such as missing data, lost data and redundant, with a focus on read, write and destroy operations' approaches controls and verifies the data at the end modeling. This verification starts until the system has finished modeling, and begun the correction begins after a passive verification is completed. In this sense, the system uses these approaches follow a certain dysfunction, produce a significant streaming over time during modelling. In addition, after each end of correction the modeler should return in beginning to make another correction for each time for other errors detected, that causes an infinite loop. The objective of this paper is to reduce this problem of infinite loop with an identify data flow anomalies and to correct the failure of each data state in an activity using the network ad-hoc methods have been used to detect the dataflow modleing anomalies. Also, the verification made by the side of applying the combining active-help verifications and Temporal logic CTL* in a model checking with a data operations guard for each process fragment. As part of this verification in a workflow-net with a data operation, Data-State concept are used to register the status of each last data operation with its activity