Paper Info
Title
Proofs-as-Model-Transformations
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.
Year
DOI
Venue
2008
10.1007/978-3-540-69927-9_15
ICMT
Keywords
Field
DocType
formal method,model transformation,model transformation specification,natural formal definition,functional program specification,functional specification,specification type,defining model transformation specification,formal notion,model instantiation relationship,type theory,functional programming,higher order
Model transformation,Intuitionistic type theory,Suite,Computer science,Formal specification,Theoretical computer science,Mathematical proof,Formal methods,Functional specification,Metamodeling
Conference
Citations 
PageRank 
References 
23
1.07
7
Authors
1
Name
Order
Citations
PageRank
Iman Poernomo142827.61