A New Approach for the Verification of BPMN Models Using Refinement Patterns

Modeling complex workflow systems, using BPMN (Business Process Modeling Notation), is quite a hard task that cannot be done in one step. The step-wise refinement technique facilitates the understanding of complex systems by dealing with the major issues before getting involved in the details. The proposed approach allows an incrementally developing of more and more detailed models with preserving the correctness of BPMN refined models at each step. Hence, we provide a formal semantics for BPMN models based on Kripke structure and BPMN refinement patterns to provide formal verification of this correctness. This verification is ensured automatically by NuSMV model Checker based on a BPMN language to NuSMV language transformation. The refinement correctness are expressed as refinement safety properties specified with LTL (Linear Temporal Logic).