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

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