Lazy Soundness Reasoning Tool Chain

Introduction

This page contains a prototypic proof-of-concept implementation of a tool chain for proving lazy soundness for business process diagrams using pi-calculus. A corresponding paper can be found here.

Approach: The toolchain provides extensions for OmniGraffle to export BPMN diagrams into an XML file. The business processes contained in the XML file can be analyzed for structural and lazy soundness. Structural soundness analyzes the graph-structure of the business process and can be informally described as follows:

A business process is structural sound if it has exactly one initial node, exactly one final node, and all other nodes lie on a path between the initial and the final node.

Lazy soundness can be informally described as follows:

A structural sound business process is lazy sound if in any case a result is provided exactly once.

Architecture

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

First of all, we use a graphical editor for creating business process diagrams. The editor is equipped with a set of BPMN stencils that are 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 analyzed for structural soundness 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 used OmniGraffle Professional as a graphical editor. OmniGraffle is fully programmable using AppleScript, which 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.

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 consider the corresponding documentation.

Quick Walk Through

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

Open OmniGraffle, select the BPMN stencils and draw the following diagram. Take care of using only elements provided by the stencils, including flows!
Select all the elements of the process.
Choose "OmniGraffle BPMN-Exporter" from the AppleScript menu. Select an appropriate target file and destination.
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).
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.
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.
Open MWB or ABC. Load your generated pi-calculus file. MWB uses input "filename", whereas ABC uses load "filename".
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.
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.
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).