Instantaneous Soundness Checking of Industrial Business Process Models

Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. Instantaneous Soundness Checking of Industrial Business Process Models. In Umeshwar Dayal, Johann Eder, Jana Koehler, and Hajo Reijers, editors, Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, September 2009. Springer-Verlag.

Authors

  • Dirk Fahland1)

  • Cédric Favre2)

  • Barbara Jobstmann3)

  • Jana Koehler4)

  • Niels Lohmann5)

  • Hagen Völzer6)

  • Karsten Wolf7)

Abstract

We report on a case study on control-flow analysis of business process models. We checked 735 industrial business process models from financial services, telecommunications and other domains. We checked these models for soundness (absence of deadlock and lack of synchronization) using three different approaches: the business process verification tool Woflan, the Petri net model checker LoLA and a recently developed technique based on SESE decomposition. We evaluate the various techniques utilized by these approaches with respect to their ability of accelerating the check. Our results show that industrial business process models can be checked in a few milliseconds, which enables tight integration of modeling with control-flow analysis. We also briefly compare the diagnostic information delivered by the different approaches.

Bibtex

@inproceedings{FahlandWJKLVW_2009_bpm,

Author = {Dirk Fahland and C{\'e}dric Favre and Barbara Jobstmann and Jana Koehler and Niels Lohmann and Hagen V{\"o}lzer and Karsten Wolf},

Booktitle = {Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings},

Editor = {Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers},

Month = sep,

Publisher = {Springer-Verlag},

Series = {Lecture Notes in Computer Science},

Title = {Instantaneous Soundness Checking of Industrial Business Process Models},

Volume = {5701},

Year = {2009}

}

Case Study

Tools

You can download the tools which we used in our case study.

Process Models

The original IBM WebSphere Business Modeler process models mentioned in the paper are available from http://www.zurich.ibm.com/csc/bit/downloads.html in the XML format used by IBM WebSphere Business Modeler.

The Petri net translations of the business processes mentioned in the paper can be downloaded in different formats.

See the UML2oWFN manual for details.

For checking soundness of these or of your own process models created in IBM WebSphere Business Modeler, you can use the IBM Pattern-based Process Model Accelerators V2.0 plugin or our compiler UML2oWFN together with a Petri net analysis tool. We give a tutorial on using UML2oWFN in our Tool Chain: UML2oWFN and LoLA.

Check Soundness with LoLA

To use LoLA to check for soundness of a process, proceed as follows:

  1. Download the most recent version of LoLA at http://service-technology.org/files/lola.

  2. Unpack LoLA by executing

tar xfz lola-1.12.tar.gz

3. Configure LoLA by executing

cd lola-1.12

./configure

4. Compile one version of LoLA to check for reachability of a state predicate by executing

make lola-statepredicate1

5. Compile another version of LoLA to check for liveness of state predicate by executing

make lola-liveprop1

Now, copy the to executables into your path.

  • To check whether the process contains lack of synchronization, execute

lola-statepredicate1 process.lola -aprocess.lola.safe.task

  • To check whether the process contains a deadlock, execute

lola-liveprop1 process.lola -aprocess.lola.fin.task

1) Humboldt-Universität zu Berlin, Unter den Linden 6, 10099 Berlin, Germany

2) , 4) , 6) IBM Zurich Research Laboratory, Säumerstrasse 4, 8803 Rüschlikon, Switzerland

3) EPF Lausanne, 1015 Lausanne, Switzerland

5) , 7) Universität Rostock, 18051 Rostock, Germany