تأیید ساختارهای جریان کار : رویکرد داخل شبکه پتری باست

While many workflow management systems have emerged in recent years, few of them provide any form of support for verification. Consequently, most workflows become operational before they have been thoroughly checked. This frequently results in runtime errors which need to be corrected on-the-fly at, typically, prohibitive costs. This paper shows how verification of a typical process control specification, which is at the heart of most workflow specifications, can benefit from state-of-the-art Petri-net based analysis techniques. To illustrate the applicability of the approach, a verification tool has been developed. This tool can download and verify the correctness of process definitions designed with Staffware, one of the leading workflow management systems.

Recent years have seen the proliferation of work owmanagement systems developed for dierent types of work ows and based on dierent paradigms (see e.g. [2, 21, 20, 22, 27, 30, 31, 41, 50]). Despite the abundance of such tools, the critical issue of work ow verication is virtually neglected. Few tools provide any form of verication support. This lack of support can be explained from the fact that the verication of work ows is hard from a computational as well as an algorithmic point of view (see e.g. [1, 7, 26]). The consequences, however, are that few work ows are thoroughly checked before they are deployed in practice, which often results in errors having to be corrected in an ad hoc fashion often at prohibitive costs. Work ow specications address many issues including data ow, exception handling, recovery etc. Hence, verication of a full work ow specication is typically not feasible. However, typically the specication of process control is at the heart of most work ow specications. Work ow specication languages need to support the specication of moments of choice, sequential execution, parallelism, synchronization, and iteration. In this paper we focus on Task Structures (see e.g. [24]) which is a powerful language for the specication of process control. Task structures can be seen as a good general representative of process control specication languages used in work owmanagement. The specication language as used in [15] is essentially the same as Task Structures. In [10, 9]Task Structures were extended with advanced work ow concepts and used for a real-life work ow application involving road closures in Queensland. There are also work ow management systems that use a language close to Task Structures. In fact, we show that there is a one-to-one correspondence between Task Structures and the diagramming technique used in Staware [45]. Staware is one of the leading work ow management systems with more than 550,000 users worldwide. In fact, according to the Gartner Group, Staware is the market leader with 25 percent of the global market [16]. Petri nets have been around since Carl Adam Petri's PhD thesis in the early sixties [37] and have found many applications in computer science. Petri nets have a rigorous mathematical foundation and a substantial body of theory for their formal analysis has been developed. In this paper thistheory is exploited and state-of-the-art Petri-net based techniques are used for the verication of Task Structures. The results provide an important impetus for the further automation of work ow verication, in particular as many sophisticated automated tools for the analysis of Petri nets exist. One such tool, Wo an [5], and its application, will be brie y discussed in this paper. In particular, it will be demonstrated how Wo an can be used for the verication of work ow specications in Staware. The organization of this paper is as follows. In section 2 the various perspectives of work ow modeling are discussed. In Section 3, Task Structures are introduced. In Section 4 Task Structures are rst mapped to Petri nets and then an extension of this mapping is described to a particular form of Petri nets, WF-nets, particularly suitable for work ow modeling. Section 5 then applies formal Petri net analysis techniques to the results of such mappings. In Section 6 we describe the functionality of Wo an and in particular the implementation of the link between Staware and Wo an. Section 7 provides a concrete case study highlighting the main aspects of the approach presented. Section 8 gives pointers to related work and Section 9 provides conclusions and some topics for future research.

In this paper, we have mapped Task Structures onto Petri nets. For verication purposes we added information about the number of parallel ows to the net by introducing a \shadow place" S and adding a start place/transition and an end place/transition. The resulting Petri net corresponds to the class of WF-nets dened in [1, 4] extended with arc weights. Since Task Structures are similar to diagramming techniques used in leading work ow management systems, the translation from Task Structures to Petri nets constitutes a basis for bridging the gap between the diagramming techniques in commercial systems and Petri-net-based analysis techniques. To illustrate this, we showed that Staware, the worlds leading work ow management system, has a diagramming technique which is very similar to Task Structures. The fact that we can map Task Structures onto WF-nets, allows for the verication of Task Structures using state-of-the-art Petri-net-based analysis techniques. In this paper, we showed that soundness property (a set of minimal requirements any Task Structure should satisfy) for Task Structures corresponds to liveness of the corresponding extended WF-net. Therefore, we can use standard Petri-net analysis tools to verify the correctness of a Task Structure. To illustrate the applicability of our approach, we developed a link between Staware and Wo an, a Petri-net-based work ow analyzer, to enable the automatic verication of work ow processes specied in Staware.