Publications 2004

  • [PDF] H. M. W. Verbeek, “Verification of wf-nets,” PhD Thesis, 2004.
    [Bibtex]
    @PhdThesis{Verbeek04,
    Title = {Verification of WF-nets},
    Author = {Verbeek, H. M. W.},
    School = {BETA},
    Year = {2004},
    Month = {June},
    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.},
    File = {BETA dissertations series:http\://www.tm.tue.nl/beta/publications/phdthesis.htm:URL;Preprint of PhD thesis:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek04.pdf:URL},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://alexandria.tue.nl/extra2/200411300.pdf}
    }
  • [PDF] H. M. W. Verbeek, W. M. P. van der Aalst, and A. Kumar, “Xrl/woflan: verification and extensibility of an xml/petri-net-based language for inter-organizational workflows,” Information technology and management (itm), vol. 5, iss. 1–2, pp. 65-110, 2004.
    [Bibtex]
    @Article{Verbeek04a,
    Title = {XRL/Woflan: Verification and Extensibility of an XML/Petri-net-based language for inter-organizational workflows},
    Author = {Verbeek, H. M. W. and Aalst, W. M. P. van der and Kumar, A.},
    Journal = {Information Technology and Management (ITM)},
    Year = {2004},
    Number = {1--2},
    Pages = {65--110},
    Volume = {5},
    Abstract = {In this paper, we present XRL/Woflan. XRL/Woflan is a software tool using state-of-the-art Petri-net analysis techniques for verifying XRL workflows. The workflow language XRL (eXchangeable Routing Language) supports cross-organizational processes. XRL uses XML for the representation of process definitions and Petri nets for its semantics. XRL is instance-based, therefore, workflow definitions can be changed on the fly and sent across organizational boundaries. These features are vital for todays dynamic and networked economy. However, the features also enable subtle, but highly disruptive, cross-organizational errors. On-the-fly changes and one-of-a-kind processes are destined to result in errors. Moreover, errors of a cross-organizational nature are difficult to repair. XRL/Woflan uses eXtensible Stylesheet Language Transformations (XSLT) to transform XRL specifications to a specific class of Petri nets, and to allow users to design new routing constructs, thus making XRL extensibe. The Petri-net representation is used to determine whether the workflow is correct. If the workflow is not correct, anomalies such as deadlocks and livelocks are reported.},
    File = {Information Technology and Management:http\://www.kluweronline.com/issn/1385-951X/current:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek04a.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://www.springerlink.com/content/l3021675x4ll2531/fulltext.pdf}
    }
  • [PDF] [DOI] H. M. W. Verbeek and R. A. van der Toorn, “Transit case study,” in 25th international conference on application and theory of petri nets (icatpn 2004), Bologna, Italy, 2004, pp. 391-410.
    [Bibtex]
    @InProceedings{Verbeek04b,
    Title = {Transit Case Study},
    Author = {Verbeek, H. M. W. and Toorn, R. A. van der},
    Booktitle = {25th International Conference on Application and Theory of Petri Nets (ICATPN 2004)},
    Year = {2004},
    Address = {Bologna, Italy},
    Editor = {Cortadella, J. and Reisig, W.},
    Month = {June},
    Pages = {391--410},
    Publisher = {Springer, Berlin, Germany},
    Series = {Lecture Notes in Computer Science},
    Volume = {3099},
    Abstract = {One of the key issues of object-oriented modeling is inheritance. It allows for the definition of a subclass that inherits features from some superclass. When considering the dynamic behavior of objects, as captured by their life cycles, there is no general agreement on the meaning of inheritance. Basten and Van der Aalst introduced the notion of life-cycle inheritance for this purpose. Unfortunately, the search tree needed for deciding life-cycle inheritance is in general prohibitively large. This paper presents a comparative study between two possible algorithms. The first algorithm uses structural properties of both the base life cycle and the potential sub life cycle to prune the search tree, while the second is a plain exhaustive search algorithm. Test cases show that the computation times of the second algorithm can indeed be prohibitively expensive (weeks), while the computation times of the first algorithm are all within acceptable limits (seconds). An unexpected result of this case study is that it shows that we need tools for checking life-cycle inheritance.},
    Doi = {10.1007/b98283},
    File = {Lecture Notes in Computer Science:http\://link.springer.de/link/service/series/0558/index.htm:URL;Volume 3099:http\://link.springer.de/link/service/series/0558/tocs/t3099.htm:URL;Applications and Theory of Petri Nets 2004:http\://www.cs.unibo.it/atpn2004:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek04b.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://www.springerlink.com/content/x2fdbaa299dp5e7r/fulltext.pdf}
    }
  • [PDF] [DOI] M. Weske, W. M. P. van der Aalst, and H. M. W. Verbeek, “Advances in business process management,” Data & knowledge engineering (dke), vol. 50, iss. 1, pp. 1-8, 2004.
    [Bibtex]
    @Article{Weske04,
    Title = {Advances in Business Process Management},
    Author = {Weske, M. and Aalst, W. M. P. van der and Verbeek, H. M. W.},
    Journal = {Data \& Knowledge Engineering (DKE)},
    Year = {2004},
    Number = {1},
    Pages = {1--8},
    Volume = {50},
    Comment = {Guest editorial},
    Doi = {10.1016/j.datak.2004.01.001},
    File = {Data and Knowledge Engineering:http\://www.sciencedirect.com/science?_ob=JournalURL&_cdi=5630&_auth=y&_acct=C000024518&_version=1&_urlVersion=0&_userid=499892&md5=90132c818879c806ad6da5399356d789:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Weske04.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2009.01.28},
    Url = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6TYX-4BJ5XYV-1-9&_cdi=5630&_user=499892&_orig=browse&_coverDate=07/31/2004&_sk=999499998&view=c&wchp=dGLbVzz-zSkWz&md5=25903ba0bbacc8c2d57c4d9a43abd28e&ie=/sdarticle.pdf}
    }

Leave a Reply