تائید کننده تفکر درست برای شبکه های جریان کاری مفهومی با داده : تشخیص زود هنگام اشتباهات با بیشترین دقت ممکن

A conceptual workflow model specifies the control flow of a workflow together with abstract data information. This model is later on refined by adding specific data information, resulting in an executable workflow which is then run on an information system. It is desirable that correctness properties of the conceptual workflow are transferable to its refinements. In this paper, we present classical workflow nets extended with data operations as a conceptual workflow model. For these nets, we develop a novel technique to verify soundness. An executable workflow is sound if from every reachable state it is always possible to terminate properly. Our technique allows us to analyze a conceptual workflow and to conclude whether there exists at least one sound refinement of it, and whether any refinement of a conceptual workflow model is sound. The positive answer to the first question in combination with the negative answer to the second question means that sound and unsound refinements for the conceptual workflow in question are possible.

Information systems are a key technology in today's organizations. Prominent examples of information systems are enterprise resource planning (ERP) systems and workflow management systems. Processes are the core of most information systems [1]. They orchestrate people, information, and technology to deliver products. In this paper, we focus on workflows. A workflow refers to the automation of a processes by an IT infrastructure, in whole or in part [2]. A workflow is usually iteratively designed following a bottom-up approach. First, the control flow of the workflow is modeled. The control flow consists of a set of coordinated tasks describing the behavior of the workflow. Later, the control flow is extended with abstract data information. The resulting model is an abstract or conceptual workflow model; it is typically constructed by a business analyst. This conceptual model can be used for purposes of documentation, communication, and analysis. It may abstract from concrete data values, such as the condition of an if-then-else construct, and it usually does not specify how concrete data values are stored. To actually execute this workflow on a workflow management system, the conceptual workflow model is instantiated with full detail—a task typically performed by business programmers (who often have insufficient background knowledge of the process) and not by the business analysts themselves. For example, the business programmer specifies concrete data values and how they are stored. The modeling of abstract and executable workflows is supported by industrial workflow modeling languages available on the market. Designing a workflow model is a complicated and error-prone task even for experienced process designers. For a fast and, therefore, cost-efficient design process, it is important that errors in the model are detected during the design phase rather than at runtime. Hence, verification needs to be applied at an early stage—that is, already on the level of the conceptual workflow model. Formal verification of a conceptual workflow model imposes two challenges. First, it requires an adequate formal model. With adequate we mean that the model captures the appropriate level of abstraction and enables efficient analysis. So the question is, how can we formalize commonly used conceptual workflow models? Second, verification must not be restricted to the control flow, but should also incorporate available data information. Thereby the conceptual workflow model may specify abstract data values that will be refined later on. Here the question is, can we verify conceptual workflows in such a way that the results hold for any possible data refinement (i.e., for all possible executable versions)? In this paper, we investigate these two questions. We focus on one of the most established requirement for workflow correctness, the soundness property [3]. Soundness guarantees that the workflow has always the possibility to terminate and every task of the workflow is coverable (i.e., can potentially be executed). Termination ensures that the workflow can during its execution neither get stuck (i.e., it is deadlock free) nor enter a loop that cannot be left (i.e., the workflow is livelock free), whereas coverable excludes dead tasks in the workflow. However, current techniques for verifying soundness are mostly restricted to the control flow and do not consider data information. To answer the first question, we propose workflow nets with data (WFD-nets) as an adequate formalism for modeling conceptual workflows. A WFD-net is a workflow net (i.e., a Petri net tailored toward the modeling of the control flow of workflows) extended with conceptual read/write/delete data operations and guards. A guard defines an additional constraint that must be fulfilled to enable a transition (i.e., a task). WFD-nets generalize our previous model from [4] by supporting arbitrary guards—previously, only predicate-negation and conjunctions were allowed. The syntax of WFD-nets is actually similar to the syntax of the Protos tool of Pallas Athenas, which is the leading process modeling tool in the Netherlands.

We have proposed workflow nets extended with data (WFD-nets) as a formalization of conceptual workflow models. We have presented algorithms to verify whether any refinement or all refinements for given WFD-net are sound. Soundness guarantees the proper termination of a WFD-net and that certain transitions are not dead. Our algorithms achieve maximal precision w.r.t. soundness, but it is possible to extend the results to cope with other definitions of soundness. Our work is can be seen a cross-fertilization of design and modeling frameworks coming from the field of process-aware information systems (PAIS) [1], and verification and abstraction approaches developed in the area of formal methods. To apply the proposed verification techniques, they must enable the verification of conceptual workflow models of industrial size. The state space of a WFD-net N is in the size of O(|S|·3|Π|·2|D|)O(|S|·3|Π|·2|D|) where |S||S| denotes the size of the state space of the underlying WF-net of N , |Π||Π| the number of predicates in N , and |D||D| the number of data elements of N. The use of hyper transitions makes the size of the model exponential in the number of states of N. We can formulate our verification target as a generalized model checking problem [36]. As a result, verification complexity is at least quadratic in the size of N. Despite the complexity, we believe that our techniques are tractable, because it has been observed that size of industrial models than the worst case complexity bound. Another requirement for applying a verification technique is the quality of the diagnosis. Business analysts need detailed feedback indicating the cause for an error in the model rather than an answer “not may-sound.” Our algorithms check the existence of a faulty situation witnessing the violation of must-soundness and may-soundness. A witness trace leading to such a faulty situation can be reported (as is standard in model checking [43]). Deriving more elaborate diagnosis results – for example, suggestions on how an error can be repaired – is an open research question and a line of further research. In ongoing work, we plan to implement the proposed verification techniques for WFD-nets in the process analysis and discovery framework ProM [44]. As ProM provides import functionality for many industrial process modeling languages, the integration of our implementation in ProM will enable us to achieve direct applicability of our framework to conceptual workflows from practice. With this implementation, we can validate our theoretical results and adjust them if necessary. In addition to control flow and data flow, resources are another important ingredient of a workflow model. For this purpose, we plan to work on extending our model to formalize the resource perspective and to adjust the presented verification techniques thereof. In addition, we want to apply our results to the verification of services—that is, reactive process models.