Embedding domain-specific modeling languages into Maude specifications

Vlad Rusu 1
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Abstract : 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.
Type de document :
Article dans une revue
Software and Systems Modeling, Springer Verlag, 2013, 12 (4), pp.847-869. 〈10.1007/s10270-012-0232-5〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

Contributeur : Mister Dart <>
Soumis le : lundi 16 janvier 2012 - 01:08:41
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : mardi 17 avril 2012 - 02:21:04


Fichiers éditeurs autorisés sur une archive ouverte




Vlad Rusu. Embedding domain-specific modeling languages into Maude specifications. Software and Systems Modeling, Springer Verlag, 2013, 12 (4), pp.847-869. 〈10.1007/s10270-012-0232-5〉. 〈hal-00660104〉



Consultations de la notice


Téléchargements de fichiers