Business Process Modeling Notation (BPMN) is becoming increasingly popular for automating processes and orchestrating people and systems. However, many process models suffer from control flow errors, such as deadlocks, livelocks, and starvation [1]. These errors hinder the correct execution of BPMN models and may be detected late in the development process, resulting in elevated costs.
In this paper, we describe a new tool, the BPMN Analyzer 2.0 1 , for analyzing BPMN process models to detect control flow errors already during modeling. Figure 1 shows an overview of the tool. The UI is based on the popular bpmn.io ecosystem, while the analysis is implemented in Rust for optimal performance and memory efficiency. We perform a breadth-first state space exploration to check soundness and safeness [2] on the fly to uncover control flow errors. Consequently, the tool can detect deadlocks, livelocks, starvation, dead activities, and lack of synchronization in BPMN models. The BPMN Analyzer is open source and accessible online alongside a video demonstration 2 [3]. tkra@hvl.no (T. Kräuter); past@hvl.no (P. Stünkel); aru@hvl.no (A. Rutle); yla@hvl.no (Y. Lamo); harald.koenig@fhdw.de (H. König) The tool can check models after each change since analysis is instantaneous according to [1], i.e., it takes 500ms or less. Furthermore, we ensure the results are comprehensible by highlighting possible violations directly in the model and displaying an interactive counterexample visualization. Finally, the tool suggests fixes for the most common control flow errors and can be extended to suggest more fixes in the future.
Fahland et al. [1] describe coverage, immediacy, and consumability as the main challenges for users unaccustomed to formal analysis. The BPMN Analyzer addresses all these challenges since it supports the most common BPMN elements used in practice (coverage), provides instantaneous results (immediacy), and a comprehensible user interface (consumability), even including suggestions for fixes. Developers of industrial BPMN software also like our tool, especially the End-to-end user journey [3]. Thus, this supports our claim that the UI is understandable for users unfamiliar with formal analysis.
In the remainder of the paper, we describe how instantaneous, comprehensible, and fixable control flow error detection is achieved in section 2. Then, we discuss tool maturity in section 3 before concluding in section 4.
The BPMN Analyzer has three main innovations: instantaneous, comprehensible, and fixable control flow error detection. In this section, we will present the innovations, and more details can be found in our extended paper [3].
We demonstrate instantaneous control flow analysis by benchmarking our tool in three scenarios. For all our benchmarks, we use the hyperfine benchmarking tool (version 1.18.0), which calculates the average runtime when executing each control flow analysis ten or more times. We ran the benchmarks on Ubuntu 22.04.4 with an AMD Ryzen 7700X processor (4.5GHz) and 32 GB of RAM (5600 MHz). All used BPMN models, our tools to generate them, and benchmarking scripts to run them are available in [3].
First, we benchmarked how our tool handles BPMN models of growing size. We generated 500 synthetic BPMN models starting with five elements up to 4000. The models repeatedly contain three activities and an exclusive/parallel block with two branches containing one activity per branch (see [3]). The BPMN Analyzer spends from 1 ms up to 9 ms for the BPMN models [3] compared to 0.7 s up to 14 s in our previous tool [4]. In summary, the runtime grows linearly with the state space.
Second, we benchmarked the tool against a synthetic data set of models that led to a state space explosion. This represents a worst-case scenario for formal analysis. We generated a data set of models [3] with a growing number of parallel branches with increasing length, like [5].
Table 1 shows the average runtime of our tool when analyzing these models. The BPMN Analyzer explores the entire state space while simultaneously analyzing the control flow, i.e., verifying soundness properties. The models' state space grows exponentially, leading to the same order of growth in runtime. Our analysis is not instantaneous anymore when approaching 17 parallel branches of length 1 (see Table 1). However, analysis is still instantaneous for more reasonable models with five parallel branches of length 5 or 3 branches of length 20. Other tools report 2-3s of runtime for most soundness properties and 30s for a model with five parallel branches [5], which took milliseconds in our tool. credit-scoring-async 31 ms 60 credit-scoring-sync 3 1 ms 140 dispatch-of-goods 3 1 ms 103 recourse 3 1 ms 77 self-service-restaurant 3 1 ms 190
Third, we applied our tool to eight realistic models, where three models (e001, e002, e020) are taken from [6], and the remaining five models are part of the Camunda BPMN for research repository 3 . Table 2 shows each model's average runtime and number of states. The BPMN Analyzer takes 1-10ms for e001, e002, and e020 [3], while [6] and [4] report 3.66-10.26s and 1-1.75s respectively. The benchmarks in [4] were run on the same hardware, while the machine used in [6] was less powerful. Our analysis is instantaneous for nearly all BPMN models since most have less than 1000 states, according to [1].
We implemented two features to make control flow analysis understandable for everyone. First, we highlight the problematic elements that cause control flow errors by directly attaching red overlays to them in the model. In addition, there is a summary panel in the top-right stating if any errors are found.
Second, we use tokens to visualize errors interactively, i.e., show an execution leading to the error. Our analysis provides sample executions resulting in the found control-flow errors, which we visualize in the editor by showing how tokens move from the process start to an erroneous state. We are unaware of other tools that visualize errors directly and allow interactions, such as stopping/resuming and restarting.
In Figure 2, the visualization has been paused just before an unsafe state was reached. One token is already located at the marked sequence flow, while a second token is currently waiting at the exclusive gateway e1. The visualization can be resumed or restarted using the play and restart on the left side. The gateway e1 will execute when resumed, resulting in two tokens at the subsequent sequence flow, i.e., an unsafe execution state. Furthermore, one can control the visualization speed using the bottom buttons next to the speedometer.
Besides detecting, highlighting, and visualizing control flow errors, the BPMN Analyzer suggests fixes like quick fixes in IDEs. Quick fixes cannot be provided for all errors, but we currently cover many patterns leading to deadlocks, lack of synchronization, message starvation, and reused end events. The quick fixes we support are described in detail in [3] and can be extended independently of the formal analysis. We are unaware of other tools that can fix identified control-flow errors.
For example, Figure 2 shows a screenshot of our tool, where quick fixes are depicted as green overlays containing a light bulb icon. A user can apply a quick fix by clicking on a green overlay and instantly see the changes regarding control flow errors. If unhappy with the result, a user can undo all changes since each quick fix is entirely revertible due to the command pattern. A user might not like a quick fix if it not only fixes an error but also has unintended side effects, such as introducing a different control flow error.
The BPMN Analyzer incorporates many findings from our previous work [4] while focusing on instantaneous and understandable error detection, as described in the previous section. The tool is open source [3], and we ensure high code quality by employing industry best practices such as rigorous static analysis and testing. Furthermore, we received positive feedback from companies in the BPMN process orchestration space [3].
In this paper, we describe the novel BPMN Analyzer that provides instantaneous, comprehensible, and fixable BPMN control flow error detection and is integrated into a popular BPMN modeling tool. We benchmarked our tool against synthetic and realistic BPMN models to demonstrate instantaneous soundness checking. We address the three main challenges, coverage, immediacy, and consumability, to provide formal analysis to non-expert users as identified in [1]. In addition, our tool offers quick fixes for common patterns that lead to control flow errors. One can understand the BPMN Analyzer as a BPMN-specific model checker, implemented in Rust paired with an intuitive user interface based on the popular bpmn.io ecosystem that is open for extension by design.
In future work, we aim to improve our tool by providing more quick fixes, considering advanced BPMN elements such as different events, and ranking quick fixes based on usefulness and previous user behavior. Finally, we aspire to test our tool in a real-world scenario to gather feedback and measure its impact on productivity.