6documents trouvés
Transformation des diagrammes d'activités SysML1.2 vers les réseaux de Petri dans un cadre MDE
D.FOURES
ISI
Rapport LAAS N°11864, Rapport de stage, Décembre 2012, 65p.
Lien : http://hal.archives-ouvertes.fr/hal-00761053
Diffusable
Plus d'informations
Résumé
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.
From sequence diagrams UML 2.x to FD-DEVS by model transformation
R.PASQUA, D.FOURES, V.ALBERT, A.NKETSA
ISI
Manifestation avec acte : European Simulation and Modelling Conference ( ESMC ) 2012 du 22 octobre au 24 octobre 2012, Essen (Allemagne), 2012, pp.37-43 , N° 12481
Lien : http://hal.archives-ouvertes.fr/hal-00781084
Diffusable
Plus d'informations
Abstract
This work transforms sequence diagrams to Finite and Deterministic DEVS (FD-DEVS) in Model-Driven En- gineering field. The main goal is the formalisation of behaviours, described with UML sequence diagram, to make verification activity by space state exploration and to make validation activity of a set of traces by simu- lation. In this context, we have chosen to elaborate a model transformation. This paper shows how, after the construction of meta-model for sequence diagrams and for Finite and Deterministic DEVS, it is possible to automate the transformation from one instance of source meta-model to one instance of destination meta-model. The source model is a sequence diagram and the target model is a FD-DEVS component. The destination model is converted into DEVSJava code to simulate its execution.
Formal compatibility of experimental frame concept and finite and deterministic DEVS model
D.FOURES, V.ALBERT, A.NKETSA
ISI
Manifestation avec acte : International Conference on Modeling Optimization & SIMulation (MOSIM 2012), Bordeaux (France), 6-8 Juin 2012, 10p. , N° 12112
Diffusable
127358Model-driven engineering approach for SysML activity diagram simulation
D.FOURES, V.ALBERT, J.C.PASCAL, A.NKETSA
ISI
Manifestation avec acte : Journées FAC'2012 (Formalisation des Activités Concurrentes), Toulouse (France), 4-5 Avril 2012, 9p. , N° 12104
Diffusable
127879Automation of SysML activity diagram simulation with model-driven engineering approach
D.FOURES, V.ALBERT, J.C.PASCAL, A.NKETSA
ISI
Manifestation avec acte : Spring Simulation Multiconference (SpringSim'12), Orlando (USA), 26-29 Mars 2012, 8p. , N° 12099
Diffusable
127061ActivityDiagram2PetriNet: transformation-based model in accordance with the OMG sysml specifications
D.FOURES, V.ALBERT, J.C.PASCAL
ISI
Manifestation avec acte : European Simulation and Modelling Conference (ESM'2011), Guimarães (Portugal), 24-26 Octobre 2011, pp.429-434 , N° 11345
Diffusable
Plus d'informations
Abstract
This study aims to automate the transformation of activity diagrams (AD) to Petri nets (PN). Based on specifications given by the Object Management Group (OMG), we have established transformation rules in ATLAS Transformation Language (ATL) to obtain a model consistent with our Petri Net meta-model (model2model). The semantic of Activity Diagram was verified with PetriNet2Tina transformation (model2text) and has allowed us to verify that was the same in the corresponding PN. This verification is done with the "model-checker" TIme petri Net Analyzer (TINA) and Linear Temporal Logic (LTL) language. The user needs only to set up the Activity Diagram from the stakeholder requirements; the transformation and verification is automatic. PetriNet formalism could enable us to provide valuable information on a Activity Diagram, to execute and simulate it.