TY - GEN

T1 - Rewriting logic semantics and verification of model transformations

AU - Boronat, Artur

AU - Heckel, Reiko

AU - Meseguer, José

N1 - Funding Information:
Acknowledgments. We cordially thank Francisco Durán for his kind help with the CRC and MTT Maude tools. We also thank the anonymous reviewers for their helpful comments and suggestions. This work has been partially supported by the NSF Grant IIS-07-20482, by the project META TIN2006-15175-C05-01, and by the project SENSORIA, IST-2005-016004.

PY - 2009

Y1 - 2009

N2 - Model transformations are used in model-driven development for mechanizing the interoperability and integration among modeling languages. Due to the graph-theoretic nature of models, the theory of graph transformation systems and its technological support provide a convenient environment for formalizing and verifying model transformations, which can then be used for defining the semantics of modelbased domain-specific languages. In this paper, we present an approach for formalizing and verifying QVT-like transformations that reuses the main concepts of graph transformation systems. Specifically, we formalize model transformations as theories in rewriting logic, so that Maude's reachability analysis and model checking features can be used for verifying them. This approach also provides a new perspective on graph transformation systems, where their formal semantics is given in rewriting logic. All the ideas presented are implemented in MOMENT2. In this way, we can define formal model transformations in the Eclipse Modeling Framework (EMF) and we can verify them in Maude. We use a model of a distributed mutual exclusion algorithm to illustrate the approach.

AB - Model transformations are used in model-driven development for mechanizing the interoperability and integration among modeling languages. Due to the graph-theoretic nature of models, the theory of graph transformation systems and its technological support provide a convenient environment for formalizing and verifying model transformations, which can then be used for defining the semantics of modelbased domain-specific languages. In this paper, we present an approach for formalizing and verifying QVT-like transformations that reuses the main concepts of graph transformation systems. Specifically, we formalize model transformations as theories in rewriting logic, so that Maude's reachability analysis and model checking features can be used for verifying them. This approach also provides a new perspective on graph transformation systems, where their formal semantics is given in rewriting logic. All the ideas presented are implemented in MOMENT2. In this way, we can define formal model transformations in the Eclipse Modeling Framework (EMF) and we can verify them in Maude. We use a model of a distributed mutual exclusion algorithm to illustrate the approach.

KW - LTL model checking

KW - MOF

KW - Maude

KW - Model and graph transformations

KW - QVT

KW - Reachability analysis

KW - Rewriting logic

UR - http://www.scopus.com/inward/record.url?scp=67650153258&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=67650153258&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-00593-0_2

DO - 10.1007/978-3-642-00593-0_2

M3 - Conference contribution

AN - SCOPUS:67650153258

SN - 9783642005923

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 18

EP - 33

BT - Fundamental Approaches to Software Engineering - 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings.

T2 - 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009

Y2 - 22 March 2009 through 29 March 2009

ER -