Abstract: The business process modeling notation(BPMN),as a standard captures business processes in the early phases of system development,instructs the designing and development.The correctness of the BPMN model is a key to influencing software success.In view that the BPMN formal model can verify the correctness of the model, an extended Petri nets model was proposed to apply model-driven development technology to realize formalization automatic execution of the BPMN model. By refining the Transition and Place elements of the basic Petri nets,and increasing the Organization Identifier and Group Identifier container,the model is not only able to describe the dynamic behaviour of the BPMN model,but also can describe the dynamic behaviours cooperation and the static organization structure of the BPMN model.This paper analyzed the elements of the extended Petri net model from metamodel structure,grammar and notation detailed,and used model-driven development to design the transformation rule from BPMN model elements to extended Petri net model elements.In order to carry out the formalization automatic executing,the executing of the transformation rule uses ATL model transformation language and the ATL transformation code runs on the Eclipse framework.Finally,the Travel Agency system was applied to demonstrate the executing result of the formalization plug(BPMN2 Extend Petrinets).

Key words: BPMN model,Model formalization,Petri nets,Model transformations