A type-theoretic framework for certified model transformations

Loading...
Thumbnail Image
Date
2010
Authors
Calegari, Daniel
Luna, Carlos
Szasz, Nora
Tasistro, Álvaro
Publisher
Universidad ORT Uruguay. Facultad de Ingeniería
DOI
ISSN
1688-8707
ISBN
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." [Abstract]
En
Thesis note
Thesis degree name
16 p.
Notes
Subject
TEOREMA AUTOMÁTICO-DEMOSTRACIÓN, TEORÍA DE TIPOS, SOFTWARE-DESARROLLO, INGENIERÍA DIRIGIDA POR MODELOS
Type
Documento de investigación
Access the full text
Citation
Calegari, D., Luna, C., Szasz, N., & Tasistro, Á. (2010). A type-theoretic framework for certified model transformations. (Documento de Investigación nro. 9). Montevideo: Universidad ORT Uruguay. Facultad de Ingeniería. Recuperado de http://rad.ort.edu.uy/handle/20.500.11968/2726
View in library
Rights license
Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)