Transformation des diagrammes d'activités SysML1.2 vers les réseaux de Petri dans un cadre MDE

Damien Foures (1)

1 LAAS-ISI - Équipe Ingénierie Système et Intégration

Cette étude cherche à automatiser la transformation des diagrammes d'activités (DA) vers les réseaux de Petri. En nous basant sur les spécifications de l'Object Management Group (OMG), nous avons établi les règles de transformation en ATLAS Transformation Langage (ATL) pour obtenir un modèle conforme à notre méta-modèle réseaux de Petri. La sémantique du diagramme d'activité a été validée à l'aide de la transformation PetriNet2Tina qui va permettre de vérifier de façon formelle la correspondance sémantique entre les deux modèles après transformation. Cette vérification est effectuée avec le "model-checker" TIme petri Net Analyser (TINA) et le langage Linear Temporal Logic (LTL). L'utilisateur devra simplement établir le diagramme d'activité à partir des exigences des parties prenantes, la transformation et la vérification étant automatiques. Le formalisme des Réseaux de Petri nous permet de fournir de précieuses informations sur le diagramme d'activité pour le jouer et le simuler.

Mots clés: ATL; Transformation; Modélisation; MDE; MDA; IDM; Automatisation; LTL; validation; verification

Domaines: Modélisation et simulation; Théorie et langage formel [cs.FL]

Damien Foures. Transformation des diagrammes d'activités SysML1.2 vers les réseaux de Petri dans un cadre MDE. 2012, 55p. ⟨hal-00761053⟩