Instantaneous, Comprehensible, and Fixable Soundness Checking of Realistic BPMN Models

TL;DR

This work tackles the problem of control-flow errors in BPMN models by introducing a Rust-implemented soundness checker with a BPMN editor frontend, delivering instantaneous verification (<500 ms) and human-friendly explanations. The method combines on-the-fly state-space exploration with pragmatic BPMN semantics encoding to keep the analysis fast while preserving correctness for soundness and safeness properties. Key contributions include interactive counterexample visualizations, direct in-model violation highlighting, and automatic quick fixes for common violations, all designed for seamless integration into existing BPMN tools. The results on synthetic and realistic BPMN models demonstrate fast performance, improved comprehensibility, and practical repair capabilities, suggesting meaningful impact for modeling practices and early error detection.

Abstract

Many business process models have control-flow errors, such as deadlocks, which can hinder proper execution. In this paper, we introduce our new soundness-checking tool that can instantaneously identify errors in BPMN models, make them comprehensible for modelers, and even suggest corrections to resolve them automatically. We demonstrate that our tool's soundness checking is instantaneous, i.e., it takes less than 500ms, by benchmarking our tool against synthetic BPMN models with increasing size and state space complexity, as well as realistic models provided in the literature. Moreover, the tool directly displays possible soundness violations in the model and provides an interactive counterexample visualization of each violation. Additionally, it provides fixes to resolve the violations found, which are not currently available in other tools. The tool is open-source, modular, extensible, and integrated into a popular BPMN modeling tool.

Figures (11)

• Figure 1: Overview of the tool
• Figure 2: BPMN model with three blocks krauterHigherorderTransformationApproach2024
• Figure 3: Soundness checking runtime for models of increasing size
• Figure 4: Models with a growing number of parallel branches and branch length
• Figure 5: Soundness violations in the analysis tool