Abstract
QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, in part due to ambiguities and omissions in the original semantics, acceptance and development of effective tool support have been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this article, we propose a QVT-R tool that complies to such semantics. Unlike any other existing tool, it also supports meta-models enriched with OCL constraints (thus avoiding returning ill-formed models) and proposes an alternative enforcement semantics that works according to the simple and predictable “principle of least change.” The implementation is based on an embedding of both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving. We also show how this technique can be applied to bidirectionalize ATL, a popular (but unidirectional) model transformation language.
Similar content being viewed by others
Notes
Download and more information about Echo is available at http://haslab.github.io/echo and in the tool demo [33].
References
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Softw. Syst. Model. 9, 69–86 (2010)
ATLAS group: ATL user guide. http://wiki.eclipse.org/ATL/User_Guide
Boronat, A., Carsí, J., Ramos, I.: Algebraic specification of a model transformation engine. FASE’06, LNCS, vol. 3922. Springer, Berlin (2006)
Bradfield, J., Stevens, P.: Recursive checkonly QVT-R transformations with general when and where clauses via the modal mu calculus. In: FASE’12, LNCS, vol. 7212, pp. 194–208. Springer, Berlin (2012)
Bradfield, J., Stevens, P.: Enforcing QVT-R with mu-calculus and games. In: FASE’13, LNCS, vol. 7793, pp. 282–296. Springer, Berlin (2013)
Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: ICFEM’12, LNCS, vol. 7635, pp. 198–213. Springer, Berlin (2012)
Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2), 283–302 (2010)
Cicchetti, A., Ruscio, D.D., Eramo, R., Pierantonio, A.: JTL: a bidirectional and change propagating transformation language. In: SLE’10, LNCS, vol. 6563, pp. 183–202. Springer, Berlin (2010)
Cunha, A., Garis, A., Riesco, D.: Translating between alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 1–21 (2013)
Cunha, A., Macedo, N., Guimarães, T.: Target oriented relational model finding. In: FASE’14, LNCS, vol. 8411, pp. 17–31. Springer, Berlin (2014)
de Lara, J., Guerra, E.: Formal support for QVT-relations with coloured petri nets. In: MoDELS’09, LNCS, vol. 5795, pp. 256–270. Springer, Berlin (2009)
Diskin, Z., Xiong, Y., Czarnecki, K., Ehrig, H., Hermann, F., Orejas, F.: From state- to delta-based bidirectional model transformations: the symmetric case. In: MoDELS’11, LNCS, vol. 6981, pp. 304–318. Springer, Berlin (2011)
Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), 17 (2007)
Frias, M.F., Pombo, C.L., Aguirre, N.: An equational calculus for Alloy. In: ICFEM’04, LNCS, vol. 3308, pp. 162–175. Springer, Berlin (2004)
Garcia, M.: Formalization of QVT-Relations: OCL-based static semantics and Alloy-based validation. In: MDSD Today 2008, pp. 21–30. Shaker (2008)
Giese, H., Wagner, R.: From model transformation to incremental bidirectional model synchronization. Softw. Syst. Model. 8(1), 21–43 (2009)
Greenyer, J., Kindler, E.: Comparing relational model transformation technologies: implementing query/view/transformation with triple graph grammars. Softw. Syst. Model. 9(1), 21–46 (2010)
Greenyer, J., Pook, S., Rieke, J.: Preventing information loss in incremental model synchronization by reusing elements. In: ECMFA’11, LNCS, vol. 6698, pp. 144–159. Springer, Berlin (2011)
Guerra, E., de Lara, J.: An algebraic semantics for QVT-relations check-only transformations. Fundam. Inform. 114(1), 73–101 (2012)
Hegedüs, Á., Horváth, Á., Ráth, I., Branco, M.C., Varró, D.: Quick fix generation for DSMLs. In: VL/HCC’11, pp. 17–24. IEEE (2011)
Hermann, F., Ehrig, H., Orejas, F., Czarnecki, K., Diskin, Z., Xiong, Y., Gottmann, S., Engel, T.: Model synchronization based on triple graph grammars: correctness, completeness and invertibility. Softw. Syst. Model. 1–29 (2013)
Hidaka, S., Hu, Z., Inaba, K., Kato, H., Nakano, K.: GRoundTram: an integrated framework for developing well-behaved bidirectional model transformations. In: ASE’11, pp. 480–483. IEEE (2011)
ikv++ technologies ag: Medini QVT. http://projects.ikv.de/qvt/
Jackson, D.: Software Abstractions: Logic, Language, and Analysis, revised edn. MIT Press, Cambridge (2012)
Jouault, F., Kurtev, I.: Transforming models with ATL. In: MoDELS’05 Satellite Events, LNCS, vol. 3844, pp. 128–138. Springer, Berlin (2005)
Jouault, F., Kurtev, I.: On the architectural alignment of ATL and QVT. In: SAC’06, pp. 1188–1195. ACM (2006)
Jouault, F., Tisi, M.: Towards incremental execution of ATL transformations. In: ICMT’10, LNCS, vol. 6142, pp. 123–137. Springer, Berlin (2010)
Kleiner, M., Fabro, M.D.D., Albert, P.: Model search: formalizing and automating constraint solving in MDE platforms. In: ECMFA’10, LNCS, vol. 6138, pp. 173–188. Springer, Berlin (2010)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)
Macedo, N.: Translating alloy specifications to the point-free style. Master’s thesis, Escola de Engenharia, Universidade do Minho, Braga, Portugal (2010)
Macedo, N., Cunha, A.: Implementing QVT-R bidirectional model transformations using Alloy. In: FASE’13, LNCS, vol. 7793, pp. 297–311. Springer, Berlin (2013)
Macedo, N., Cunha, A., Pacheco, H.: Towards a framework for multidirectional model transformations. In: EDBT/ICDT’14 Workshops, CEUR Workshop Proceedings, vol. 1133, pp. 71–74. CEUR-WS.org (2014)
Macedo, N., Guimarães, T., Cunha, A.: Model repair and transformation with Echo. In: ASE’13, pp. 694–697. IEEE (2013)
Macedo, N., Pacheco, H., Cunha, A., Oliveira, J.N.: Composing least-change lenses. ECEASST 57, 1–18 (2013)
Meertens, L.: Designing constraint maintainers for user interaction. In: Third Workshop on Programmable Structured Documents. Tokyo University (2005)
Milicevic, A., Jackson, D.: Preventing arithmetic overflows in alloy. In: ABZ’12, LNCS, vol. 7316, pp. 108–121. Springer, Berlin (2012)
Montaghami, V., Rayside, D.: Extending alloy with partial instances. In: ABZ’12, LNCS, vol. 7316, pp. 122–135. Springer, Berlin (2012)
Near, J.P., Jackson, D.: An imperative extension to alloy. In: ASM’10, LNCS, vol. 5977, pp. 118–131. Springer, Berlin (2010)
Oliveira, J.N.: Extended static checking by calculation using the pointfree transform. In: LerNet’08, LNCS, vol. 5520, pp. 195–251. Springer, Berlin (2009)
OMG: MOF 2.0 query/view/transformation specification (QVT), version 1.1 (2011). http://www.omg.org/spec/QVT/1.1/
OMG: OMG unified modeling language (UML), version 2.4.1 (2011). http://www.omg.org/spec/UML/2.4.1/
OMG: OMG object constraint language (OCL), version 2.3.1 (2012). http://www.omg.org/spec/OCL/2.3.1/
OMG: OMG meta object facility (MOF), version 2.4.1 (2013). http://www.omg.org/spec/MOF/2.4.1/
Rayside, D., Chang, F.S.H., Dennis, G., Seater, R., Jackson, D.: Automatic visualization of relational logic models. ECEASST 7, 1–14 (2007)
Sasano, I., Hu, Z., Hidaka, S., Inaba, K., Kato, H., Nakano, K.: Toward bidirectionalization of ATL with GRoundTram. In: ICMT’11, LNCS, vol. 6707, pp. 138–151. Springer, Berlin (2011)
Stevens, P.: Bidirectional model transformations in QVT: semantic issues and open questions. Softw. Syst. Model. 9(1), 7–20 (2010)
Stevens, P.: A simple game-theoretic approach to checkonly QVT relations. Softw. Syst. Model. 12(1), 175–199 (2013)
Straeten, R.V.D., Puissant, J.P., Mens, T.: Assessing the Kodkod model finder for resolving model inconsistencies. In: ECMFA’11, LNCS, vol. 6698, pp. 69–84. Springer, Berlin (2011)
Tata Research Development and Design Centre: ModelMorf. http://www.tcs-trddc.com/trddc_website/ModelMorf/ModelMorf.htm
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: TACAS’07, LNCS, vol. 4424, pp. 632–647. Springer, Berlin (2007)
Voigt, K.: Structural graph-based metamodel matching. Ph.D. thesis, University of Desden (2011)
Xiong, Y., Liu, D., Hu, Z., Zhao, H., Takeichi, M., Mei, H.: Towards automatic model synchronization from model transformations. In: ASE’07, pp. 164–173. ACM (2007)
Acknowledgments
This work is funded by ERDF—European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by national funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020532. The first author is also sponsored by FCT grant SFRH/BD/69585/2010. The authors would also like to thank all anonymous reviewers for the valuable comments and suggestions.
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by Prof. Gabriele Taentzer.
Rights and permissions
About this article
Cite this article
Macedo, N., Cunha, A. Least-change bidirectional model transformation with QVT-R and ATL. Softw Syst Model 15, 783–810 (2016). https://doi.org/10.1007/s10270-014-0437-x
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10270-014-0437-x