up: Publications |
Abstract |
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:
@incollection{djeddai12:_integ_formal_devel_dsls_meta_model, 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, Boualem}, doi = {10.1007/978-3-642-33609-6_7}, url = {http://www.irit.fr/~Martin.Strecker/Publications/medi2012.html}, publisher = {Springer Berlin Heidelberg}, keywords = {Model Driven Engineering; Model Transformation; Formal Methods; Verification}, pages = {55-66} }Journal version:
@article{djeddai13:_integ_formal_devel_dsls_meta_model, 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 Meta-Modeling}, url = {http://www.irit.fr/~Martin.Strecker/Publications/medi2012.html}, 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 \cite{djeddai12:_integ_formal_devel_dsls_meta_model}} }
Last modified: Tue Nov 12 22:52:09 CET 2013 |