This paper concerns a formal encoding of the Object Management Group’s Complete Meta-Object Facility (CMOF) in order to provide a more trustworthy software development lifecycle for Model Driven Architecture (MDA). We show how a form of constructive logic can be used to provide a uniform semantics of metamodels, model transformation specifications, model transformations and black-box transformation tests. A model’s instantiation of a metamodel within the MOF is treated using the logic’s realizability relationship, a kind of type inhabitation relationship that is expressive enough to characterize constraint conformance between terms and types. These notions enable us to formalize the notion of a correct model instantiation of a metamodel with constraints. We then adapt previous work on snapshot generation to generate input models from source metamodel specification with the purpose of testing model transformations.

A constructive approach to testing model transformations / C. Fiorentini, A. Momigliano, M. Ornaghi, I. Poernomo - In: Theory and practice of model transformations / [a cura di] L. Tratt, M. Gogolla. - Berlin : Springer, 2010. - ISBN 9783642136870. - pp. 77-92 (( Intervento presentato al 3. convegno International Conference on Model Transformation (ICMT) tenutosi a Malaga nel 2010.

A constructive approach to testing model transformations

C. Fiorentini
Primo
;
A. Momigliano
Secondo
;
M. Ornaghi
Penultimo
;
2010

Abstract

This paper concerns a formal encoding of the Object Management Group’s Complete Meta-Object Facility (CMOF) in order to provide a more trustworthy software development lifecycle for Model Driven Architecture (MDA). We show how a form of constructive logic can be used to provide a uniform semantics of metamodels, model transformation specifications, model transformations and black-box transformation tests. A model’s instantiation of a metamodel within the MOF is treated using the logic’s realizability relationship, a kind of type inhabitation relationship that is expressive enough to characterize constraint conformance between terms and types. These notions enable us to formalize the notion of a correct model instantiation of a metamodel with constraints. We then adapt previous work on snapshot generation to generate input models from source metamodel specification with the purpose of testing model transformations.
generation
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
2010_icmt.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 293.92 kB
Formato Adobe PDF
293.92 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/146885
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 12
social impact