This repository contains the sources for our paper (pre-print) published at ICGT-2023 together with additional information below.

The corresponding BPMN Analyzer tool is available here.

★ The paper received the Best Software Science Paper Award. ★

Our wiki describes the BPMN formalization in more detail, accompanied by many examples of BPMN models and graph transformation rule examples.

Process termination is implemented by the following graph transformation rule in Groove:

The rule is called Terminate and is automatically added during graph grammar generation. The dashed red borders mark parts of negative application conditions, grey parts remain untouched, blue parts are deleted, and green parts are added.

General BPMN properties can be checked in the web-based tool, which runs Groove in the cloud (no local installation needed).

The Implementation section shows a screenshot with an example verification result.

The atomic property Unsafe is implemented by the following graph condition in Groove:

The property matches whenever two tokens of one process snapshot have the same position (but have different identities).

The atomic property AllTerminated is implemented by the following graph condition in Groove:

The property matches whenever there is no process snapshot in the state running. All process snapshots are terminated, i.e., have no tokens.

Defining atomic propositions directly in BPMN Analyzer by distributing tokens over the process model has not been implemented yet. Thus, for the time being, custom properties have to be checked in Groove by defining atomic propositions there.

The BPMN Analyzer is available online here.

The source code of the BPMN Analyzer is available here and instructions how to run it locally on your machine can be found here.

The experiments are described here.

The wiki describes our comprehensive test suite to test our coverage of BPMN features.

Feel free to contact me for further information.

The instructions to run the experiments can be found here.