Formal verification of business processes with temporal and resource constraints

The correctness of business process models is critical for IT system development. The properties of business processes need to be analyzed when they are designed. In particular, business processes usually have various constraints on time and resources, which may cause serious problems like bottlenecks and deadlocks. In this paper, we propose an approach based on the model checking technique for verifying business process models with temporal and resource constraints. First, we extend Business Process Modeling Notation (BPMN) to handle these constraints. Then, we provide a mapping of the business process models described with this extended BPMN onto timed automata that can be verified by the UPPAAL model checker. This approach helps to eliminate various problems with time and resources in the early phase of development, and enables the quality assurance of business process models.