Formal verification using model checking is a process to ensure that the BPMN design model is free of deadlock and other undesirable properties that can cause a system crash. Safeness and soundness are the important properties that have to be verified of the BPMN design model. Formal verification is a complicated procedure involving the fomal language for model abstraction and the use of model checking tools, including the techniques for handling large-scale BPMN design model and state space explosion problem. An automated transformation can reduce the flaws, time consumption, and complexity of the large-scale BPMN design mode, as well as overcoming the state space explosion problem. This paper proposes the safeness and soundness verification techniques for BPMN design model using model checking. Colored Petri Net (CPN) is used to describe an abstract model. A BPMN partitioning technique and a hierarchical verification are used for avoiding state space explosion problem. To validate and analyze BPMN design model, the transformation technique and state space generator have been implemented as a BPMN verification framework which is a viable option for the software process designers and suitable for large-scale BPMN design model verification.
