Assembling the Proofs of Ordered Model Transformations

Maribel Fernández
Jeffrey Terrell

In model-driven development, an ordered model transformation is a nested set of transformations between source and target classes, in which each transformation is governed by its own pre and post- conditions, but structurally dependent on its parent. Following the proofs-as-model-transformations approach, in this paper we consider a formalisation in Constructive Type Theory of the concepts of model and model transformation, and show how the correctness proofs of potentially large ordered model transformations can be systematically assembled from the proofs of the specifications of their parts, making them easier to derive.

In Barbora Buhnova, Lucia Happe and Jan Kofroň: Proceedings 10th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA 2013), Rome, Italy, March 23, 2013, Electronic Proceedings in Theoretical Computer Science 108, pp. 63–77.
Published: 20th February 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: