The Business Process Modeling Notation (BPMN) is a standardized notation for modeling business processes. We are currently developing a precise execution semantics for BPMN, using graph rewrite rules. In addition to that we developed two transformations. We developed one transformation from BPMN to the workflow system YAWL, which allows BPMN models to be executed in workflow. We developed another transformation from BPMN to the Petri net formalism, which allows BPMN models to be formally analyzed.
We are in the process of defining a complete formalization of the BPMN 2.0 execution semantics, using graph rewrite rules. The benefit of formalizing the execution semantics by means of graph rewrite rules is that there is a strong relation between the execution semantics rules that are informally specified in the BPMN 2.0 standard and their formalization. This makes it easy both to understand and to validate the formalization. We also implemented the formalization in a tool called GrGen. Having a formalized and implemented execution semantics in terms of graph rewrite rules supports simulation, animation and execution of BPMN 2.0 models. In particular we aim to use the formal execution semantics to verify workflow engines and service orchestration and choreography engines that use BPMN 2.0 for modeling the processes that they execute.
The current version of the formal execution semantics supports most of the BPMN control-flow elements. It is described in this technical report. The implementation of the execution semantics is available through a virtual machine that is made available here. We developed a series of screencasts to explain how the execution semantics works and how it can be accessed. These screencasts can be found here.
A graphical user interface to the execution semantics, along with some example BPMN models can be found here.
The BPMN to YAWL transformer can transform BPMN models into YAWL models. The BPMN models must be constructed with the STP BPMN modeler. Both the transformer and the modeler are Eclipse plugins and must be installed with Eclipse (see below). YAWL is a workflow engine. The result of the transformation can be executed directly by YAWL, it can be opened in the YAWL editor and it can be opened in ProM for analysis.
The BPMN to Petri net transformer can transform BPMN models to Petri net models. It implements the theory presented in this technical report. The BPMN models can be constructed using the ILOG BPMN Modeler. The following figure shows a screenshot of an example BPMN model in the ILOG BPMN Modeler.
The resulting Petri net models can be opened in ProM. This tool will automatically lay-out the models and allows various forms of analysis, such as deadlock and livelock checks, to be performed on the Petri net. The following figure shows what the transformed model from the previous figure looks like in ProM.
The tool can be started from the command prompt. Starting it without arguments, will show the acceptable arguments. The example BPMN files from this technical report are included in the zip file. The behaviour from the figures above can be transformed by typing: