Abstract
We present a framework based on the Calculus of Inductive Constructions (CIC) and its associated tool the Coq proof assistant to allow certification of model transformations in the context of Model-Driven Engineering (MDE). The approached is based on a semi-automatic translation process from metamodels, models and transformations of the MDE technical space into types, propositions and functions of the CIC technical space. We describe this translation and illustrate its use in a standard case study. © 2011 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Calegari, D., Luna, C., Szasz, N., & Tasistro, Á. (2011). A type-theoretic framework for certified model transformations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6527 LNCS, pp. 112–127). Springer Verlag. https://doi.org/10.1007/978-3-642-19829-8_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
