Embedding domain-specific modeling languages into Maude specifications

Rusu, Vlad

Document type :

Article dans une revue scientifique: Article original

DOI :

10.1007/s10270-012-0232-5

Title :

Embedding domain-specific modeling languages into Maude specifications

Author(s) :

Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]

Journal title :

Software and Systems Modeling

Pages :

847-869

Publisher :

Springer Verlag

Publication date :

2013

ISSN :

1619-1366

HAL domain(s) :

Informatique [cs]/Systèmes embarqués

English abstract : [en]

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) ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Files

https://hal.inria.fr/hal-00660104/document
Open access
Access the document

https://api.istex.fr/document/DCB98AED24FF76F1AC17C00A3DF7691B1300AA5B/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/DCB98AED24FF76F1AC17C00A3DF7691B1300AA5B/fulltext/pdf?sid=hal
Open access
Access the document

https://hal.inria.fr/hal-00660104/document
Open access
Access the document

https://api.istex.fr/document/DCB98AED24FF76F1AC17C00A3DF7691B1300AA5B/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/DCB98AED24FF76F1AC17C00A3DF7691B1300AA5B/fulltext/pdf?sid=hal
Open access
Access the document

document
Open access
Access the document

paper.pdf
Open access
Access the document

pdf
Open access
Access the document

document
Open access
Access the document

paper.pdf
Open access
Access the document

Embedding domain-specific modeling languages ... BibTeX CSV Excel RIS

Files

Embedding domain-specific modeling languages ...

BibTeX

CSV

Excel

RIS