This repository contains the sources for our article published in Logical Methods in Computer Science (LMCS) and additional artifacts below.
This article is an extended version of a paper published at ICGT-2023, which received the ★ Best Software Science Paper Award ★.
The corresponding BPMN Analyzer tool is described below. Other additional artifacts of this article are also listed below, following the section structure of the article.
A demonstration of our tool is available on YouTube.
Our wiki describes the BPMN formalization in more detail, accompanied by many examples of BPMN models and graph transformation rule examples.
The following graph condition in Groove implements process termination:
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 BPMN Analyzer tool subsection shows a screenshot with an example verification result.
To check this property, we generate the state space of the GT system and analyze it to see if each activity has been executed at least once. If this property is not fulfilled, the activity is highlighted in red in the BPMN model. See, for example, the BPMN Analyzer tool subsection.
The "shipGoodsTwice" proposition results in the following graph condition in Groove:
You can check that this state is never reached using the CTL proposition AG(!shipGoodsTwice).
The "noShipment" proposition results in the following graph condition in Groove:
You can check that a shipment always occurs using the CTL proposition !AG(noShipment).
The GT systems for the examples can be found here ending in .gps.
After downloading and unzipping, you can each Gt system in Groove to explore the state space in detail and run model checking.
The BPMN Analyzer is available online here. The wiki describes our comprehensive test suite to test our coverage of BPMN features.
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 BPMN Analyzer is built using different libraries we have created. These libraries are also helpful in other contexts and have thus been shared independently of the tool:
- An editor library for defining a snapshot/state of a running BPMN process using tokens and process snapshots: token-bpmn (npm)
- An extension of the BPMN metamodel, the Token Editor, adding process snapshots and tokens: token-bpmn-moddle (npm)
- A library to generate graph transformation systems currently implemented for Groove: graph rule generation (Maven central)
The performance tests are described here.
The scalability tests are described here.