On the Marriage of Theory and Practice in Data-Aware Business Processes via Low-Code
Ali Nour Eldin, Benjamin Dalmas, Walid Gaaloul
TL;DR
This work tackles the verification of data aware BPMN by introducing BPMN-ProX, a low-code extension that injects data semantics into BPMN and enables both formal verification and runtime testing. The approach combines front end data rich modeling based on BPDML with an encoding to SQL-like specifications and uses MCMT for formal verification plus Spock for runtime unit tests. Contributions include data source definitions for persistent and volatile data, verification aware control flow, modeling constraints, encoding rules, guard automation, automated unit tests, and a proof of concept translator to MCMT. This framework aims to empower non technical analysts to design, verify, and execute data aware processes with stronger guarantees and closer alignment between theory and practice.
Abstract
In recent years, there has been a growing interest in the verification of business process models. Despite their lack of formal characterization, these models are widely adopted in both industry and academia. To address this issue, formalizing the execution semantics of business process modeling languages is essential. Since data and process are two facets of the same coin, and data are critical elements in the execution of process models, this work introduces Proving an eXecutable BPMN injected with data, BPMN-ProX. BPMN-ProX is a low-code testing framework that significantly enhances the verification of data-aware BPMN. This low-code platform helps bridge the gap between non-technical experts and professionals by proposing a tool that integrates advanced data handling and employs a robust verification mechanism through state-of-the-art model checkers. This innovative approach combines theoretical verification with practical modeling, fostering more agile, reliable, and user-centric business process management.