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.

In this paper we propose an approach for transforming UML statechart and collaboration diagrams to colored Petri nets models. This transformation aims to bridge the gap between informal notation (UML diagrams) and more formal notation (colored Petri nets models) for analysis purpose. It produces highly-structured, graphical, and rigorously-analyzable models that facilitates early detection of errors like deadlock, livelock, etc ... The approach is based on graph transformation since the input and output of the transformation process are graphs. The meta-modeling tool ATOM3is used. An example illustrates our approach.