UML2oWFN - Translating UML2 Activity Diagrams to Petri nets

UML2oWFN is a tool to translate UML2 Activity Diagrams to Petri nets with the aim of verifying business process and service choreographies.

Understand UML2oWFN

UML2oWFN implements a fairly standard pattern based translation from a UML2 activity diagram subset into Petri nets. Its strength is its back-end where it can modify and extend the generated Petri net for specific kinds of analysis tasks such as verifying soundness of processes with LoLA: A Low Level Petri Net Analyzer and the workflow analysis tool Woflan.

The semantics that is implemented in UML2oWFN is explained in Translating UML2 Activity Diagrams to Petri Nets.

Case Studies

We used UML2oWFN in a case study for analyzing the soundness of over 700 industrial business process created in the IBM WebSphere Business Modeler. The results of this case study and the used process models are available here.

References

The following pages provide further information about UML2oWFN, the underlying theory, and case-studies.

Tool chains

You may use UML2oWFN in the following tool chains:

Download and Install

UML2oWFN is free software and is licensed under the GNU Affero General Public License. Other licenses can be negotiated with the author.

Wendy is written in C/C++ and packaged by the GNU Autotools. To compile and install, unpack the tarball and execute the following commands:

./configure

make

make install

For more information, please have a look at the files README, INSTALL, and REQUIREMENTS which are part of the source release.

Change Log

A detailed change log is available here.

Use UML2oWFN

UML2oWFN is a prototypic implementation and has no graphical interface. Instead, UML2oWFN is controlled with a few command line parameters.

Quick Introduction

To quickly get started with UML2oWFN, you can follow the Tool Chain: UML2oWFN and LoLA which describes how to invoke UML2oWFN and analyze the output with LoLA. The subsequent sections give a more detailed overview on the features of UML2oWFN.

Exporting IBM WebSphere Business Modeler processes

In order to generate proper input files for UML2oWFN, open the process library you wish to verify in the IBM WebSphere Business Modeler, right click on the library or a single process you wish to verify, and choose “File > Export” to open the export wizard. In the wizard

  • select “WebSphere Business Modeler Export”,

  • then choose “WebSphere Business Modeler XML (.xml)”, and

  • on the following page choose a target directory for export (e.g. ./process/lib.xml) and select (or confirm) the part of the process library you wish to export

  • “Finish” and wait for the IBM WebSphere Business Modeler to complete.

You will now find an .xml file at the designated location, e.g. ./process/lib.xml.

Translate a process library to Petri net

To translate a process library to Petri nets, type

uml2owfn -i <lib.xml> -f <pnformat> -o

with <lib.xml> being the absolute or relative path to a IBM WebSphere Business Modeler XML file, e.g. ./process/lib.xml and with <pnformat> being one of the supported Petri net formats of UML2oWFN. For instance try -f lola to generate a Petri net in the input format of our model checker LoLA: A Low Level Petri Net Analyzer. If GraphViz dot is available on your system, you may use -f dot to create a graphical representation of each Petri net in .png format.

Manual

The manual of UML2oWFN provides a detailed overview on all features of UML2oWFN and how they can be controlled via the command line. It also covers a number of use cases like the analysis of soundness with different termination semantics or the soundness analysis with Woflan. You find the most recent manual in .pdf format here.

Bugs

Bugs can be reported at the UML2oWFN project page or via e-mail to uml2owfnservice-technologyorg.