تشخیص صحت مدل جریان کاری معنا شناختی

Nowadays, organizations automate their business processes with workflow models that can be enacted using workflow management systems (WFMSs). For organizations it is essential to ensure the correct operation of workflow models at design time, before the workflow models get enacted. An incorrect operational workflow can dissatisfy customers and fixing the errors can be very costly, certainly compared to the costs of fixing the workflow model before it is deployed. Correctness of a workflow model can be verified by exhaustively checking all possible executions. Detected errors should be diagnosed, for instance by providing an error path that shows the cause of the error, such that errors can be repaired in a quick and effective way [1]. Workflow models can reference different perspectives [2]. Most workflow modeling and verification approaches only consider the control flow perspective [1], [3], [4], [5], [6], [7], [8], [9] and [10], which is about the order in which the individual activities of a business process are executed. Another relevant perspective is the dataflow perspective [11], which details the flow of data among activities subject to certain constraints. The dataflow perspective is important because data constraints influence the possible executions of activities [11] and in turn, the execution of activities results in certain data constraints being enforced. An effective means to express data constraints is to annotate activities in a workflow model with pre and postconditions that specify the effect on the data state for each activity. For instance, in the Sarbanes–Oxley Act of 2002, the internal audit department takes the lead and works alongside workflow owners for each process that has a direct effect on the data for the financial reporting. Annotating activities inside these processes with pre and postconditions facilitates compliance checking to ensure that workflows are properly designed. Only recently, approaches for verifying workflow models with dataflows have been proposed [11], [12], [13], [14] and [15]. However, these approaches do not consider diagnosis of dataflow errors. Diagnosing dataflow errors is complex due to the interplay between control flow and dataflow dependencies, as we explain in Section 2 with an example. The goal of this paper is to develop an approach for diagnosing the correctness of semantic workflow models, containing activities whose effects are formally specified using pre and postconditions. An activity can start if the execution of the workflow model has reached the activity and its precondition is satisfied. Upon completion, the activity delivers data that satisfies its postcondition. An execution of the workflow can reach an activity whose precondition is not satisfied. In that case the execution gets stuck at the activity and fails. We distinguish between two different notions of correctness to diagnose such dataflow errors: • May-correctness. A workflow model is may-correct if every activity can be executed at least once, so there is an execution in which the activity is done. • Must-correctness. A workflow model is must-correct if every possible execution that reaches an activity satisfies the precondition of the activity. The diagnosis is performed at design-time, using Artificial Intelligence techniques to compute the execution instances allowed by a workflow model. For diagnosis, the workflow model is translated into two models: (1) an Integer Programming model (IP model), to determine the different instances of execution of the workflow, and (2) the preconditions and postconditions of the activities are modeled as constraints in a Constraint Satisfaction Problem (CSP) [16], following a BNF grammar in order to avoid any ambiguity. This paper makes several contributions: • Workflow data graphs are proposed as a formalism for modeling semantic workflows with pre and postconditions for the activities. These conditions are modeled as constraints according to a well-defined grammar in BNF. • Two correctness notions for workflow data graphs, may and must-correctness, are proposed and novel diagnosis algorithms are developed for verifying may and must-correctness. The algorithms are complete: neither false positives nor false negatives are generated. Moreover, the algorithms offer precise diagnosis of the detected errors, indicating the execution causing the error where the workflow gets stuck. • The approach has been implemented in the DiagFlow tool, presented in [1]. The tool reads XPDL models [17] in which the semantics of activities and the corresponding dataflow are specified using extended attributes. This paper is organized as follows. Section 2 presents a motivating example to illustrate the concepts of may and must-correctness. Section 3 introduces workflow data graphs as a formal model for semantic workflows and defines may and must-correctness on workflow data graphs. Section 4 defines the IP and CSP formulations of a workflow data graph. The process of diagnosis is explained, and two algorithms are presented. The diagnosis of the motivating example is performed. Section 5 gives implementation details. Section 6 shows experimental results. Section 7 presents an overview of related work found in the literature. And finally, conclusions are drawn and future work is proposed in Section 8.

To engineer workflow models with dataflows in a dependable way, diagnosis of correctness is of utmost importance. To that end, we have proposed workflow data graphs as formalization of semantic workflow models together with two correctness notions, may and must-correctness, that can be verified for workflow data graphs. Workflow data graphs model semantic workflows by extending workflow graphs with pre and postconditions for the activities. We also proposed two correctness notions, may and must-correctness, for workflow data graphs. Next, we have presented a diagnosis approach to check may and must-correctness, which consists of several phases. First, preprocessing is applied to detect basic data anomalies. Then, the workflow data graph is translated into an IP formulation that models the executable instances, and into a CSP formulation that models the data states acceptable according to the pre and postconditions of the activities. The combined IP and CSP model can be efficiently solved using Constraint Programming techniques. In case of an error, feedback is provided in the form of an error path showing where the workflow gets stuck under certain conditions over the dataflow. Such feedback provides valid information for the workflow designer to fix future errors before the workflow is deployed. The approach is complete, so it always generates accurate feedback in case of an error. The approach has been implemented by extending the DiagFlow tool [1]. The tool diagnoses workflow models in an extended XPDL format. The XPDL extension is needed to store the semantic information of each workflow, adding the dataflow with the pre and postconditions in the activities. Performance evaluation of the tool shows that the algorithms scale well for large workflow models with dataflows, despite the high worst-case complexity of solving constraint satisfaction programs. As future work, we plan to extend the workflow data graph model with OR gateways. Likewise, we would also like to offer additional feedback to the end user in case of a violation, making easier the job of fixing the problem which causes the abnormal behavior. Another interesting extension is to consider stochastic behavior or timing behavior of activities, to improve the accuracy of the analysis.