Table of Contents

Verification of WF-nets

H.M.W. Verbeek
PhD Thesis. Technische Universiteit Eindhoven, Eindhoven, The Netherlands, 2004.

Abstract

The workflow process definition (WPD) of a workflow management system (WFMS) is an important concept in this thesis. If we compare a WFMS to a conveyor belt system, then a WPD can be compared to a physical layout of the conveyor belts. Thus, both a WPD and a physical layout determine how items are moved around in the corresponding system.

However, a WPD can be far more complex than a layout of a conveyor belt system, because a conveyor belt system is forced to adhere to physical constraints, whereas a WFMS is not: A conveyor belt system is tangible and moves tangible work items around, whereas a WFMS, being a piece of software, is intangible and moves intangible information items (cases) around. For example, in a WFMS, cases can be copied with ease, which enables the parallel processing of multiple tasks on one case.

Unfortunately, todays WFMSs have almost no support for the verification of a WPD, even though there is a clear need for such a verification support. Because a WPD can be very complex, it may contain (very subtle) errors. If an erroneous WPD is put into production, then it might take a while before somebody realizes that there is something wrong, as the entire process is hidden in the WFMS. Only anticipated errors can be detected by the WFMS itself, the remaining errors can only be detected after having requested some reports from the WFMS and only if these reports contain sufficient information to detect the errors.

This thesis presents the WPD verification tool Woflan and its supporting concepts. Woflan maps a WPD onto a workflow net (WF-net, which is a Petri net with some additional requirements) and can verify, before the WPD is taken into production, the soundness property and four inheritance relations for the resulting WF-net. Note that he mappings used by Woflan should be of high quality, as the results obtained for the WF-net should be transferable to the originating WPD. This thesis presents such high-quality mappings for a number of commercial WFMSs (IBM MQSeries Workflow, Staffware, COSA Workflow), for a commercial BPR tool (Protos), and for a research workflow prototype (XRL).

The soundness property is a minimal property any WPD should satisfy, and consists of the following requirements: (i) whatever happens, every case can be completed, (ii) after a case has been completed, no dangling references are left behind to that case, and (iii) every part of the WPD is necessary for some case. Woflan exploits an existing relation between soundness and the (in Petri-net world well-known) boundedness and liveness properties for diagnosis purposes. Based on this relation, this thesis introduces a diagnosis process for the soundness property, and a concept of behavioral error sequences. The diagnosis process guides the designer of an unsound WPD towards correcting this WPD, using diagnostic information like the behavioral error sequences. These sequences pinpoint decisions in the WPD that, when taken into production, lead to a violation of the soundness property. This thesis presents a number of case studies that have put several mappings, the diagnosis process, and the behavioral error sequences to the test. From these case studies, we conclude that Woflan successfully guides the designer of an unsound WPD towards correcting that WPD.

The four inheritance relations can be used to guarantee that two WPDs behave in a similar way: If two WPDs share such a relation, then cases can be transferred between the WPDs without problems. Woflan implements algorithms to compute these four relations. However, a straightforward exhaustive search algorithm for computing the most complex relation, the life-cycle inheritance relation, can lead to excessive processing times. This thesis presents a backtracking algorithm that aims to alleviate this problem of excessive processing times for computing the life-cycle inheritance relation. This thesis also presents a number of case studies that have put both algorithms to the test. From these case studies, we conclude that the backtracking algorithm effectively reduces excessive processing times. From one of these case studies, we also concluded that the life-cycle inheritance relation can be very subtle and, therefore, hard to check for humans (even for experts). Therefore, we conclude that we need a tool like Woflan to check this inheritance relation.

Download PDF (6.7 MB)