Generation of Inductive Types from Ecore Metamodels - CentraleSupélec Accéder directement au contenu
Chapitre D'ouvrage Année : 2019

Generation of Inductive Types from Ecore Metamodels

Résumé

When one wants to design a language and related supporting tools, two distinct technical spaces can be considered. On the one hand, model-driven tools like Xtext or MPS automatically provide a compilation infrastructure and a full-featured integrated development environment. On the other hand, a formal workbench like a proof assistant helps in the design and verification of the language specification. But these two technical spaces can hardly be used in conjunction. In the paper, we propose an automatic transformation that takes an input Ecore metamodel, and generates a set of inductive types in Gallina and Vernacular , the language of the Coq proof assistant. By doing so, it is guaranteed that the same abstract syntax as the one described by the Ecore metamodel is used, e.g., to formally define the language's semantics or type system or set up a proof-carrying code infrastructure. Improving over previous state of the art, our transformation supports structural elements of Ecore, with no restriction. But our transformation is not injective. A benchmark evaluation shows that our transformation is effective , including in the case of real-world metamodels like UML and OCL. We also validate our transformation in the context of an ad-hoc proof-carrying code infrastructure.
Fichier principal
Vignette du fichier
Modelsward2018_Model__CCIS___HAL_.pdf (197.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02021361 , version 1 (15-02-2019)

Identifiants

  • HAL Id : hal-02021361 , version 1

Citer

Jérémy Buisson, Seidali Rehab. Generation of Inductive Types from Ecore Metamodels. Model-Driven Engineering and Software Development. MODELSWARD 2018., pp.308-334, 2019. ⟨hal-02021361⟩
71 Consultations
301 Téléchargements

Partager

Gmail Facebook X LinkedIn More