Experiment with a type-theoretic approach to the verification of model transformations

"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.

Subject

TEORÍA DE TIPOS, TEOREMA AUTOMÁTICO-DEMOSTRACIÓN, SOFTWARE-DESARROLLO, INGENIERÍA DIRIGIDA POR MODELOS

Type

Documento de investigación

Citation

Calegari, 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/2727

Rights license

Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)

Collections

Documentos de Investigación

Full item page