Towards an Automatic Verification of BPMN Model Semantic Preservation During a Refinement Process

In this paper, we present a refinement approach for business processes specified with Business Process Modeling Notation (BPMN). The Business process or workflow refinement approach is a step-wise modeling approach which is composed of a set of abstraction levels. Each refinement step corresponds to an abstract level of a BPMN model. For each refined workflow model, we analyze, automatically, the workflow change impact using NuSMV model checker. The change impact concerns the semantic preservation of workflow models during the refinement process. We talk about workflow data and control flow dependencies. To realize this analysis, we have to transform at each level of modeling refinement, the BPMN model to a Kripke structure formalizing, hence, the semantics of the refined business process model.