2017-02-082017-02-082009Calegari, D., Luna, C., Szasz, N. & Tasistro, Á. (2009). Experiment with a type-theoretic approach to the verification of model transformations. (Documento de Investigación nro. 8). Montevideo: Universidad ORT Uruguay. Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/27271688-8707http://hdl.handle.net/20.500.11968/2727"This paper presents ongoing work on the application of constructive type theory for safe development in Model-Driven Engineering. In particular, we put into practice a certification framework based on the Calculus of Inductive Constructions (CIC) as follows: we first describe methods for representing metamodels and specifications of model transformations as types and then outline principles for representing given transformations, written in a certain transformation language, as functions in CIC. Then properties of these functions are proven, including their correctness with respect to sufficiently expressive specifications, thereby providing a semiformal way to verify the original transformations. We carry out a concrete case taken from an on-line base of basic examples and patterns of use of the ATL transformation language, implementing it on machine using the Coq proof assistant." [Abstract][20] p.https://creativecommons.org/licenses/by-nc-nd/4.0/TEORÍA DE TIPOSTEOREMA AUTOMÁTICO-DEMOSTRACIÓNSOFTWARE-DESARROLLOINGENIERÍA DIRIGIDA POR MODELOSDocumento de investigaciónLicencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)