The extended abstract of this paper has been published as a preprint on EasyChair. The follow up paper was published at ICGT-2023.
The following tables depict how graph transformation rules for BPMN-FlowNodes are generated. It depicts BPMN-FlowNodes on the left and the corresponding rule generation template on the right.
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.
BPMN-specific properties currently have to be checked in Groove due to an unresolved bug and unfinished implementation.
- Make sure Java is installed on your machine to run Groove (tested with Java version 1.8.0_301)
- Clone/download this repository.
- Start Groove by running the following command in this directory:
java -jar artifacts\groove-5_8_1\bin\Simulator.jar
- Load a graph grammar. You can generate one using the tool below and unzip it on your local machine.
- Run LTL verification by copying one of the desired properties (listed below) and right-clicking in the LTS-Simulation tab. Select
Verify < Check LTL property (full state space)and paste the copied LTL property.
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).
Verify the following LTL property in Groove for safeness:
G(!Unsafe)
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.
Verify the following LTL property in Groove for option to complete:
F(G(AllTerminated))
Defining atomic propositions directly in the tool 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.
Adding this feature is planned for the full version of the paper due to the current time constraints.
The tool is available online here.
The sourcecode of the tool is available here and instructions how to run it locally on your machine can be found here.
The test classes of the testsuite can be found in the subproject generator here. The BPMN files (see bpmnModelsSemanticsTest) and generated graph grammars from the BPMN models can be found here.
- Groove Demo: Basic functionality.
- Groove Demo: Editing Graphs and Rules.
- Groove Demo: Type Graphs.
Feel free to contact me for further information.