An automatic approach to transform BPMN models to Pi-Calculus

In order to automate Business Processes Modeling, the last research works in workflow technology have resulted in the identification of a number of models (workflow patterns) that describe the behavior of Business Processes. Like any new trend, the Business Process approach raises many expectations and many positions. BPMN (Business Process Modeling Notation) has been used to describe graphically such patterns. However, BPMN notation lacks verification tools which allow anomalies and errors detection such as deadlock and multiple repetition situations. On the other hand, formal methods, such as Pi-Calculus, have powerful tools for verifying such situations. In this paper, we propose an automatic approach to transform the basic workflow patterns into their equivalent Pi-Calculus code for the analysis purposes. To achieve this goal, we use the Model-Driven Engineering (MDE) approach which is mainly based on Meta-modeling and Model Transformations. The graph transformation tool AToM3 is used. Our approach is illustrated through an example.