Embedding domain-specific modeling languages into Maude specifications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Software and Systems Modeling Année : 2013

Embedding domain-specific modeling languages into Maude specifications

Résumé

We propose a formal approach for the definition and analysis of domain-specific modelling languages (DSML). The approach uses standard model-driven engineering artifacts for defining a language's syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by translating them to the Maude language: metamodels and models are mapped to equational specifications, and model transformations are mapped to rewrite rules between such specifications, which are also expressible in Maude thanks to Maude's reflective capabilities. These mappings provide us, on the one hand, with abstract definitions of the MDE concepts used for defining DSML, which naturally capture their intended meanings; and, on the other hand, with equivalent executable definitions, which can be directly used by Maude for formal verification. We also study a notion of operational semantics-preserving model transformations, which are model transformations between two DSML that ensure that each execution of a transformed instance is matched by an execution of the original instance. We propose a semidecision procedure, implemented in Maude, for checking the semantics-preservation property. We also show how the procedure can be adapted for tracing finite executions of the transformed instance back to matching executions of the original one. The approach is illustrated on xSPEM, a language for describing the execution of activities constrained by time, precedence, and resource availability.
Fichier principal
Vignette du fichier
paper.pdf (300.07 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-00660104 , version 1 (16-01-2012)

Identifiants

Citer

Vlad Rusu. Embedding domain-specific modeling languages into Maude specifications. Software and Systems Modeling, 2013, 12 (4), pp.847-869. ⟨10.1007/s10270-012-0232-5⟩. ⟨hal-00660104⟩
131 Consultations
126 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More