دانلود مقاله ISI انگلیسی شماره 21678
ترجمه فارسی عنوان مقاله

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

عنوان انگلیسی
Verification Of Workflow Task Structures: A Petri-net-baset Approach
کد مقاله سال انتشار تعداد صفحات مقاله انگلیسی
21678 2000 27 صفحه PDF
منبع

Publisher : Elsevier - Science Direct (الزویر - ساینس دایرکت)

Journal : Information Systems, Volume 25, Issue 1, March 2000, Pages 43–69

ترجمه کلمات کلیدی
تأیید - ساختارهای وظیفه - شبکه های پتری - جریان کار
کلمات کلیدی انگلیسی
Verification, Task Structures, Petri Nets, Workflow
پیش نمایش مقاله
پیش نمایش مقاله  تأیید ساختارهای جریان کار : رویکرد داخل شبکه پتری باست

چکیده انگلیسی

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 di erent types of work ows and based on di erent 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 Sta ware [45]. Sta ware is one of the leading work ow management systems with more than 550,000 users worldwide. In fact, according to the Gartner Group, Sta ware 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 Sta ware. 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 Sta ware 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 Sta ware, 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 Sta ware and Wo an, a Petri-net-based work ow analyzer, to enable the automatic veri cation of work ow processes speci ed in Sta ware.