Formal verification of time-bounded BPMN model with message broker using timed automata

Modern business processes are growing their complexity due to concurrency and parallelism of both digital and manual processes with synchronous and asynchronous communications. Therefore, their timing behaviors are hard to predict and verify. Business Process Model and Notation (BPMN) is widely used for business process modeling. However, BPMN is still lacking support for incorporating time constraints that are crucial properties for real-world applications where the execution times of tasks vary but are critical to business competitiveness. In this article, an extension to the standard BPMN is proposed to specify lower and upper bounds of execution times on the task elements, called Time-Bounded BPMN (TBBP), along with transformation rules to timed automata, which can be automatically transformed using the TBBPTA Tool developed in this work. This extension enables the use of the UPPAAL model checking tool to verify properties in terms of time constraints, including deadlock, safety, liveness, and reachability. To demonstrate the practical applicability of our approach, several small test cases were used to validate transformation and verification with sample TCTL queries. In addition, four case studies of complex systems are presented to illustrate how TBBP can be applied to asynchronous communications involving multiple systems, including message brokers. These case studies serve as sample prototypes for verifying asynchronous processes in distributed systems using our TBBP. Our approach bridges the gap between business process modeling and formal verification and demonstrates the potential of applying time-bounded analysis to asynchronous systems in distributed environments.