UML2oWFN is a tool to translate UML2 Activity Diagrams to Petri nets with the aim of verifying business process and service choreographies.
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.
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.
The following pages provide further information about UML2oWFN, the underlying theory, and case-studies.
|UML, formal semantics, Petri nets, publication, Dirk Fahland, UML2oWFN, LoLA|
You may use UML2oWFN in the following tool chains:
|UML, tool chain, UML2oWFN, LoLA|
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.
A detailed change log is available here.
UML2oWFN is a prototypic implementation and has no graphical interface. Instead, UML2oWFN is controlled with a few command line parameters.
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.
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.
To translate a process library to Petri nets, type
uml2owfn -i <lib.xml> -f <pnformat> -o
<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 (see below). 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
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.