Paper Info
Title
Integrating a Formal Development for DSLs into Meta-Modeling.
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 aiming at easing the specification and understanding of software systems. Moreover, these languages and concomitant environments permit to automatically generate graphical interfaces or editors for Domain Specific Languages 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 detailed and represented in a formal description. Our approach is implemented in the Eclipse environment and illustrated with a case study.
Year
DOI
Venue
2012
10.1007/978-3-642-33609-6_7
J. Data Semantics
Keywords
DocType
Volume
generic transformation process,ecore model,formal frame,model-driven engineering,eclipse environment,domain specific languages,formal development,formal method,software engineering,bidirectional transformation rule,software system
Conference
3
Issue
ISSN
Citations 
3
1861-2040
2
PageRank 
References 
Authors
0.42
15
3
Name
Order
Citations
PageRank
Selma Djeddai130.78
Martin Strecker2468.08
Mohamed Mezghiche32511.68