Abstract
As the complexity of model transformation (MT) grows, the need to count on formal semantics of MT languages also increases. Firstly, formal semantics provide precise specifications of the expected behavior of transformations, which are crucial for both MT users (to be able to understand them and to use them properly) and MT tool builders (to develop correct MT engines, optimizers, etc.). Secondly, we need to be able to reason about the MTs to prove their correctness. This is specially important in case of large and complex MTs (with, e.g., hundreds or thousands of rules) for which manual debugging is no longer possible. In this paper we present a formal semantics to the ATL model transformation language using rewriting logic and Maude, which allows addressing these issues. This formalization provides additional benefits, such as enabling the simulation of the specifications or giving access to the Maude toolkit to reason about them.
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.
References
The AtlanMod Team: ATL (2010), http://www.eclipse.org/m2m/atl/doc/
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Eclipse (ATL), http://www.eclipse.org/m2m/atl/atlTransformations/
Jouault, F., Bézivin, J.: KM3: A DSL for Metamodel Specification. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 171–185. Springer, Heidelberg (2006)
Troya, J., Vallecillo, A.: Formal Semantics of ATL Using Rewriting Logic (Extended Version). Universidad de Málaga (2010), http://atenea.lcc.uma.es/Descargas/ATLinMaude.pdf
Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236(1), 35–132 (2000)
Stevens, P.: Bidirectional model transformations in QVT: Semantic issues and open questions. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 1–15. Springer, Heidelberg (2007)
Rivera, J.E., Vallecillo, A., Durán, F.: Formal specification and analysis of domain specific languages using Maude. Simulation: Transactions of the Society for Modeling and Simulation International 85(11/12), 778–792 (2009)
Roldán, M., Durán, F.: Representing UML models in mOdCL. Manuscript (2008), http://maude.lcc.uma.es/mOdCL
di Ruscio, 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, Nantes, France (2006)
Baresi, L., Spoletini, P.: On the use of Alloy to analyze graph transformation systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 306–320. Springer, Heidelberg (2006)
Anastasakis, K., Bordbar, B., Küster, J.M.: Analysis of Model Transformations via Alloy. In: Baudry, B., Faivre, A., Ghosh, S., Pretschner, A. (eds.) Proceedings of the 4th MoDeVVa workshop Model-Driven Engineering, Verification and Validation, pp. 47–56 (2007)
Poernomo, I.: Proofs-as-model-transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 214–228. Springer, Heidelberg (2008)
Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Handbook of graph grammars and computing by graph transformation, foundations, vol. I, pp. 313–400 (1997)
Schürr, A., Winter, A.J., Zündorf, A.: The PROGRES approach: language and environment. In: Handbook of graph grammars and computing by graph transformation: applications, languages, and tools, vol. 2, pp. 487–550 (1999)
Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 18–33. Springer, Heidelberg (2009)
Boronat, A., Meseguer, J.: An algebraic semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)
Durán, F., Lucas, S., Meseguer, J.: MTT: The Maude Termination Tool (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313–319. Springer, Heidelberg (2008)
Durán, F., Meseguer, J.: A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications. In: Proc. of WRLA 2010. LNCS, Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Troya, J., Vallecillo, A. (2010). Towards a Rewriting Logic Semantics for ATL. In: Tratt, L., Gogolla, M. (eds) Theory and Practice of Model Transformations. ICMT 2010. Lecture Notes in Computer Science, vol 6142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13688-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-13688-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13687-0
Online ISBN: 978-3-642-13688-7
eBook Packages: Computer ScienceComputer Science (R0)