Team : Quentin G. & Théo Pirouelle

This mini-project consists in producing a verification chain of process models SimplePDL in order to check their consistency, in particular to know if the process described can be terminated or not. To answer this question, we use the model-checking tools defined on Petri nets through the Tina toolbox. We will translate a process model into a Petri net.

The main steps are the following:

1. Definition of the metamodels with Ecore
2. Definition of the static semantics with OCL
3. Use of the infrastructure provided by EMF to manipulate the models
4. Definition of concrete textual syntaxes with Xtext
5. Definition of graphical concrete syntaxes with Sirius
6. Definition of a model-to-model transformation (M2M) with Java and with ATL
7. Definition of model-to-text transformations (M2T) with Acceleo

For this project, we use various tools such as the Tina toolbox or the Eclispe Modeling Project IDE (Eclipse version with modeling tools).

Download links :

• Eclispe Modeling Project
• Tina toolbox