up: Publications

Integrating a Formal Development for DSLs into Meta-modeling

Selma Djeddai, Martin Strecker, Mohamed Mezghiche

Medi 2012


Formal methods (such as interactive provers) are increasingly used in software engineering. They offer a formal frame that guarantees the correctness of developments. Nevertheless, they use complex notations that might be difficult to understand for unaccustomed users. On the contrary, visual specification languages use intuitive notations and allow to specify and understand software systems. Moreover, they permit to easily generate graphical interfaces or editors for Domain Specific Languages (DSLs) starting from a meta-model. However, they suffer from a lack of precise semantics. We are interested in combining these two complementary technologies by mapping the elements of the one into the other.

In this paper, we present a generic transformation process from functional data structures, commonly used in proof assistants, to Ecore models and vice-versa. This translation method is based on Model-Driven Engineering and defined by a set of bidirectional transformation rules. These rules are presented with an illustrating example, along with an implementation in the Eclipse environment.
Online Copy

Conference version: PDF

Journal version (preprint) PDF. The final publication is available from Springer Link.

BibTeX Entry

Conference version:

  author =       {Djeddai, Selma and Strecker, Martin and Mezghiche, Mohamed},
  title =        {Integrating a Formal Development for {DSLs} into Meta-modeling},
  booktitle =    {Model and Data Engineering (MEDI)},
  year =         {2012},
  isbn =         {978-3-642-33608-9},
  volume =       {7602},
  series =       {Lecture Notes in Computer Science},
  editor =       {Abelló, Alberto and Bellatreche, Ladjel and Benatallah,
  doi =          {10.1007/978-3-642-33609-6_7},
  url =
  publisher =    {Springer Berlin Heidelberg},
  keywords =     {Model Driven Engineering; Model Transformation; Formal
                  Methods; Verification},
  pages =        {55-66}
Journal version:
  year =         2013,
  issn =         {1861-2032},
  journal =      {Journal on Data Semantics},
  doi =          {10.1007/s13740-013-0030-4},
  title =        {Integrating a Formal Development for DSLs into
  url =
  publisher =    {Springer Berlin Heidelberg},
  keywords =     {Model-driven engineering; Model transformation; Formal
                  methods; Verification},
  author =       {Djeddai, Selma and Strecker, Martin and Mezghiche, Mohamed},
  pages =        {1-13},
  note =         {Journal version of

Last modified: Tue Nov 12 22:52:09 CET 2013