Detecting structural errors in BPMN process models

Business Process Modeling Notation (BPMN) has emerged as a standard notation to express the business process models. A lack of formal semantics in the BPMN can cause the syntactic and structural errors. The former requires less effort to be checked, while the later usually needs a complex state-space analysis to prove some properties, like the deadlock-freedom and the livelock-freedom. In this paper, we present an approach based on model checking for the automated verification of business process models. We illustrate the deadlocks, livelocks, and multiple termination problems, which can help the business modelers to avoid structural errors.