ABSTRACT As the size and the complexity of business process models are an important driver of error probability, it is recommended to split large models into smaller models. Hence, we propose, in this paper, to develop business process models by refinement. A refinement is a transformation of a source model to a target model expressed in the same modeling language. This transformation should preserve the semantics of the source model to provide semantically correct target model. Thus, we propose, in this paper, a domain specific language based on Business Process Model and Notation (BPMN) language for developing by refinement business process models correct‐by‐construction. Hence, we propose (i) a formal syntax throughout a context‐free grammar , (ii) axiomatic semantics to ensure the refinement correction when building business process models, (iii) operational semantics in terms of Kripke structure permitting formal verification of provided models to check their reliability. The Kripke structure supports the verification of behavioral requirements represented by the Computational Tree Logic (CTL) temporal logic and verified by NuSMV model checker. Based on these semantics, we prove the validity of the compiler that we have developed to assist developers when building their correct models and to transform these models to NuSMV code to prove their reliability.

In this paper we introduce a description mechanism for specifying the refinement approach for Business Process Modeling and Notations(BPMN). We present at each level of abstraction the syntax of this BPMN models by a context-free grammar. After that, for each refined BPMN, we analyze, automatically the change impact using NuSMV model checker. The change impact concerns the semantic preservation of BPMN models during the refinement process.

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).