Abstract
This paper provides an overview of how to develop model transformations that are “provably correct” with respect to a given functional specification. The approach is based in a mathematical formalism called Constructive Type Theory (CTT) and a related synthesis formal method known as proofs-as-programs. We outline how CTT can be used to provide a uniform formal foundation for representing models, metamodels and model transformations as understood within the Object Management Group’s Meta-Object Facility (MOF 2.0) and Model Driven Architecture (MDA) suite of standards [6, 8]. CTT was originally developed to provide a unifying foundation for logic, data and programs. It is higher-order, in the sense that it permits representation and reasoning about programs, types of programs and types of types. We argue that this higher-order aspect affords a natural formal definition of metamodel/model/model instantiation relationships within the MOF. We develop formal notions of models, metamodels and model transformation specifications by utilizing the logic that is built into CTT. In proofs-as-programs, a functional program specification is represented as a special kind of type. A program is provably correct with respect to a given specification if it can be typed by that specification. We develop an analogous approach, defining model transformation specifications as types and provably correct transformations as inhabitants of specification types.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Akehurst, D.H., Kent, S., Patrascoiu, O.: A relational approach to defining and implementing transformations between metamodels. Software and System Modeling 2(4), 215–239 (2003)
Constable, R., Mendler, N., Howe, D.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986) (Accessed May 2003), http://www.cs.cornell.edu/Info/Projects/NuPrl/book/doc.html
Favre, L.: Foundations for mda-based forward engineering. Journal of Object Technology 4(1), 129–153 (2005)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Mottu, J.-M., Baudry, B., Le Traon, Y.: Mutation Analysis Testing for Model Transformations. In: Rensink, A., Warmer, J. (eds.) ECMDA-FA 2006. LNCS, vol. 4066, pp. 376–390. Springer, Heidelberg (2006)
Mukerji, J., Miller, J.: MDA Guide Version 1.0.1. Object Management Group (2003)
OMG. Meta Object Facility (MOF) Specification. Object Management Group (2000)
OMG. Meta Object Facility (MOF) Core Specification, Version 2.0. Object Management Group (January 2006)
Poernomo, I.: A Type Theoretic Framework for Formal Metamodelling. In: Reussner, R., Stafford, J.A., Szyperski, C.A. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol. 3938, pp. 262–298. Springer, Heidelberg (2006)
Poernomo, I., Crossley, J., Wirsing, M.: Adapting Proofs-as-Programs: The Curry-Howard Protocol. Monographs in computer science. Springer, Heidelberg (2005)
Rivera, J., Vallecillo, A.: Adding behavioural semantics to models. In: The 11th IEEE International EDOC Conference (EDOC 2007), Annapolis, Maryland, USA, pp. 169–180. IEEE Computer Society, Los Alamitos (2007)
Ruscio, D.D., Jouault, F., Kurtev, I., Bézivin, J., Pierantonio, A.: Extending AMMA for supporting dynamic semantics specifications of DSLs. Technical Report 06.02, Laboratoire d’Informatique de Nantes-Atlantique (LINA), Nantes, France (April 2006)
Simons, A.J.H.: The theory of classification. part 3: Object encodings and recursion. Journal of Object Technology 1(4), 49–57 (2002)
Thirioux, X., Combemale, B., Crégut, X., Garoche, P.-L.: A framework to formalise the mde foundations. In: Proceedings of TOWERS 2007, Zurich, June 25 2007, pp. 14–30 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poernomo, I. (2008). Proofs-as-Model-Transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds) Theory and Practice of Model Transformations. ICMT 2008. Lecture Notes in Computer Science, vol 5063. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69927-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-69927-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69926-2
Online ISBN: 978-3-540-69927-9
eBook Packages: Computer ScienceComputer Science (R0)