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 Fahland¹⁾

• Cédric Favre²⁾

• Barbara Jobstmann³⁾

• Jana Koehler⁴⁾

• Niels Lohmann⁵⁾

• Hagen Völzer⁶⁾

• Karsten Wolf⁷⁾

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

Case Study

Tools

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

• LoLA: A Low Level Petri Net Analyzer, a short tutorial is at the bottom of this page

• Original Woflan or alternatively with the Woflan-Plugin in ProM (including a tutorial)

• IBM WebSphere Business Modeler, IBM Pattern-based Process Model Accelerators V2.0, plugin and step-by-step tutorial (including installation instructions)

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.

• PNML, full processes or structurally reduced processes

• LoLA file format, full processes or structurally reduced processes. For each process, three files are given:

  • process.lola – the Petri net in LoLA's file format

  • process.lola.fin.task – a task to check for deadlocks

  • process.lola.safe.task – a task to check for lack of synchronization

• Woflan file format, full processes

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

3. Configure LoLA by executing

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

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

Now, copy the to executables into your path.

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

• To check whether the process contains a deadlock, execute

¹⁾ Humboldt-Universität zu Berlin, Unter den Linden 6, 10099 Berlin, Germany

²⁾ , ⁴⁾ , ⁶⁾ IBM Zurich Research Laboratory, Säumerstrasse 4, 8803 Rüschlikon, Switzerland

³⁾ EPF Lausanne, 1015 Lausanne, Switzerland

⁵⁾ , ⁷⁾ Universität Rostock, 18051 Rostock, Germany