Business Process Technology

Prof. Dr. Mathias Weske

>> Piworkflow > WhyPi > PiIntro > SyntaxSemantics > ProcessMapping > InteractionMapping > Routing > Interaction > LazySoundness > WeakSoundness > Simulator > Reasoner

Reasoning Tool Chain

This page provides a prototypic tool chain for deciding lazy soundness for business process diagrams using pi-calculus.

• 07/16/2007: Provided software under GPL v3, added weak_sound.rb and relaxed_sound.rb.
• 02/01/2007: Updated pi-calculus converter (lazy_sound.rb,struct_sound.rb).

Approach

A business process diagrams (BPD) is created graphically using the Business Process Modeling Notation (BPMN). The BPDs are then exported to an intermediate XML file that provides a generic abstraction from concrete modeling notations. The business processes contained in the XML file can already be checked for structural constraints like connectedness of the nodes. To prove lazy soundness, the XML file is converted to a pi-calculus formalization. The formalizations are then applied to prove lazy soundness using existing tools.

Architecture

The figure below depicts the tool dependencies and document flows in our tool chain. Tools or scripts are shown as rectangles, whereas documents are denoted as notes. The components developed by our group are shown inside the dotted area.

First of all, we utilize a graphical editor for designing business process diagrams. The editor is equipped with a set of BPMN stencils annotated with additional information. Based on this information, an XML exporter script is able to generate an XML description of the business process diagram by interacting with the editor. The XML representation of the business process can already be proved to be structural sound by a structural soundness checker script. Furthermore, it can be used as input for a pi-calculus converter script that maps the XML file to a proprietary ASCII notation representing pi-calculus processes. The file containing the pi-calculus processes can then directly be used as an input for existing pi-calculus tools for reasoning.

Technically, our feasibility study has been developed on Mac OS X. We utilized OmniGraffle Professional as a graphical editor. OmniGraffle is fully programmable using AppleScript that we used for implementing the XML exporter. Both, OmniGraffle and AppleScript, provide an easy and convenient way of designing and exporting business process diagrams. The pi-calculus converter and the structural soundness checker have been implemented as Ruby scripts, so they are OS-independent. The pi-calculus tools compatible with our scripts are MWB and ABC, the two major reasoners for pi-calculus. Both are also available on various platforms.

Tool Chain

OmniGraffle (Graphical Editor)

OmniGraffle is a commercial diagramming application for Mac OS X. A demo version is available at http://www.omnigroup.com/applications/omnigraffle/. The stencils and scripts have been tested with version 4.1.1. For those of you who don't have a Mac yet, we are working on other editors, too (Eclipse-based, maybe VISIO export).

BPMN Stencils

The BPMN stencils for OmniGraffle 4 can be found here. Please unzip and place them into your ~/Library/Application Support/OmniGraffle/Stencils folder.

The following subset of the BPMN is currently supported:

OmniGraffle BPMN Exporter

The AppleScript for exporting BPMN diagrams from OmniGraffle 4 to XML can be found here. Please place it in your ~/Library/Scripts/Application/OmniGraffle or ~/Library/Scripts/Application/OmniGraffle Pro folder, depending on your version of OmniGraffle. Enable your AppleScript menu by browsing to /Applications/Apple Script/ and start Apple Script Utilility. Check Enable Script Menu. While you have OmniGraffle as the active application, you should find an entry labeled OmniGraffle BPMN-Exporter in your scripts menu.

Structural and Lazy Soundness Pi-Calculus Converter

The Ruby script for checking business processes contained in the XML document to be structural sound and for converting the XML document to a pi-calculus ASCII notation can be found here. Both require Ruby 1.8.2 (preinstalled on Mac OS X 10.4). Unzip the scripts into a folder.

Reasoning Tools

The pi-calculus reasoning tools currently compatible are MWB and ABC (both are free available). MWB can be downloaded at http://www.it.uu.se/research/group/mobility/mwb . Download the latest sources from package and follow the installation instructions. ABC can be downloaded at http://lampwww.epfl.ch/~sbriais/abc/abc.html . Both require a functional programming language, OCaml for ABC and SML/NJ for MWB. PLEASE USE EXACTLY THE VERSIONS STATED AT ABC/MWB WEBSITES! ABC might be easier to install for novices. REMARK: Both tools are command line only.

Quick Walk Through

After having set up the tool chain as described above, you can now simply follow our walk through, or "Hello World" example.

1. Open OmniGraffle, select the BPMN stencils and draw the following diagram. Take care of using only elements provided by the stencils, including flows!

2. Select all the elements of the process.

3. Choose "OmniGraffle BPMN-Exporter" from the AppleScript menu. Select an appropriate target file and destination.

4. Open a terminal and switch to the folder where you placed the scripts (the following steps can be followed on other operating systems by downloading the XML file provided here).

5. Type ruby struct_sound input_file; i.e. ruby struct_sound omni-export.xml if you have everything in one folder. This command checks if the business process contained in your XML file is structural sound.

6. Type ruby lazy_sound input_file output_file; i.e. ruby lazy_sound omni-export.xml agents.pi. This command generates a lazy soundness annotated pi-calculus representation of your business process.

7. Open MWB or ABC. Load your generated pi-calculus file. MWB uses input "filename", whereas ABC uses load "filename".

8. Type weq N(i,o) S_LAZY(i,o) to decide weak open bisimulation between N(i,o) and S_LAZY(i,o). If both are equal, your business process used to generate the pi-calculus file is lazy sound.

9. Try different processes by modifying the OmniGraffle diagram or change the XML file directly. What about additional activities, gateways, or events? More ready-made examples (incl. XML files and PDF files of the business processes) can be downloaded here.

10. When using MWB or ABC always keep in mind that weak open bisimulation is undecidable in general, so not all inputs will give a result.

Printable | Imprint | Login