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.

翻译：许多业务流程模型存在控制流错误（如死锁），这些错误可能阻碍其正常执行。本文介绍了一款新型正确性检查工具，该工具能够即时识别BPMN模型中的错误，使建模者易于理解错误成因，并能自动提供修正建议。通过对规模与状态空间复杂度递增的合成BPMN模型及文献提供的实际模型进行基准测试，我们证明该工具的正确性检查具有即时性——检测时间均低于500毫秒。此外，该工具可直接在模型中显示潜在的正确性违反情况，并为每种违反提供交互式反例可视化。值得强调的是，本工具还能提供当前其他工具尚未具备的违规修复方案。该工具具有开源、模块化、可扩展的特性，并已集成至主流BPMN建模工具中。