Using model checking to control the structural errors in BPMN models

The emergence of BPMN as a standard notation to express the business processes is based on its simplicity of notations and its exhaustive expressiveness. Nevertheless the lack of formal semantics in the BPMN can cause syntactic and structural errors. The former requires less effort to be checked, while the later usually requires attention to prove some properties, like deadlock-freedom and livelock-freedom. In this paper, we address the issue of detecting the structural errors with an approach based on model checking. It verifies the soundness of business process model and helps the business modelers to avoid the deadlocks, livelocks, and multiple terminations errors.