Experiment with a type-theoretic approach to the verification of model transformations
| dc.creator | Calegari, Daniel | es |
| dc.creator | Luna, Carlos | es |
| dc.creator | Szasz, Nora | es |
| dc.creator | Tasistro, Álvaro | es |
| dc.date.accessioned | 2017-02-08T19:29:21Z | |
| dc.date.available | 2017-02-08T19:29:21Z | |
| dc.date.issued | 2009 | es |
| dc.description.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] | es |
| dc.format.extent | [20] p. | es |
| dc.identifier.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 | es |
| dc.identifier.issn | 1688-8707 | es |
| dc.identifier.uri | http://hdl.handle.net/20.500.11968/2727 | |
| dc.language | en | es |
| dc.publisher | Universidad ORT Uruguay. Facultad de Ingeniería | es |
| dc.relation.ispartofseries | Documento de Investigación | es |
| dc.relation.ispartofseriesno | nro. 8 | es |
| dc.rights.license | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) | es |
| dc.rights.uri | https://creativecommons.org/licenses/by-nc-nd/4.0/ | es |
| dc.subject | TEORÍA DE TIPOS | es |
| dc.subject | TEOREMA AUTOMÁTICO-DEMOSTRACIÓN | es |
| dc.subject | SOFTWARE-DESARROLLO | es |
| dc.subject | INGENIERÍA DIRIGIDA POR MODELOS | es |
| dc.title | Experiment with a type-theoretic approach to the verification of model transformations | es |
| dc.type | Documento de investigación | es |