Abstract
Refinement is a central notion in computer science, meaning that some artefact S can be safely replaced by a refinement R, which preserves S’s properties. Having available techniques and tools to check transformation refinement would enable (a) the reasoning on whether a transformation correctly implements some requirements, (b) whether a transformation implementation can be safely replaced by another one (e.g. when migrating from QVT-R to ATL), and (c) bring techniques from stepwise refinement for the engineering of model transformations.
In this paper, we propose an automated methodology and tool support to check transformation refinement. Our procedure admits heterogeneous specification (e.g. PaMoMo, Tracts, OCL) and implementation languages (e.g. ATL, QVT), relying on their translation to OCL as a common representation formalism and on the use of model finding tools.
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.
Similar content being viewed by others
References
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Software and Systems Modeling 9(1), 69–86 (2010)
Anastasakis, K., Bordbar, B., Küster, J.M.: Analysis of model transformations via alloy. In: MODEVVA 2007 (2007)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1998)
Bézivin, J., Büttner, F., Gogolla, M., Jouault, F., Kurtev, I., Lindow, A.: Model transformations? Transformation models! In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 440–453. Springer, Heidelberg (2006)
Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ‘off-the-shelf’ SMT solvers. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 432–448. Springer, Heidelberg (2012)
Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 198–213. Springer, Heidelberg (2012)
Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software 83(2), 283–302 (2010)
Cabot, J., Clarisó, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. In: ASE 2007, ACM (2007)
Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: OCL Workshop, vol. 12, pp. 69–83 (2004)
Clavel, M., Egea, M., de Dios, M.A.G.: Checking Unsatisfiability for OCL Constraints. Electronic Communications of the EASST 24, 1–13 (2009)
Guerra, E.: Specification-driven test generation for model transformations. In: Hu, Z., de Lara, J. (eds.) ICMT 2012. LNCS, vol. 7307, pp. 40–55. Springer, Heidelberg (2012)
Guerra, E., de Lara, J., Kolovos, D., Paige, R., dos Santos, O.: Engineering model transformations with transML. Software and Systems Modeling (2012) (in press)
Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F.: A visual specification language for model-to-model transformations. In: VL/HCC 2010, pp. 119–126. IEEE CS (2010)
Guerra, E., de Lara, J., Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Schönböck, J., Schwinger, W.: Automated verification of model transformations based on visual contracts. Autom. Softw. Eng. 20(1), 5–46 (2013)
Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT (2012)
Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: A model transformation tool. Sci. Comp. Pr. 72(1-2), 31–39 (2008)
Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290–306. Springer, Heidelberg (2011)
OMG OCL Specification, version 2.3.1 (Document formal/2012-01-01) (2012)
Orejas, F., Wirsing, M.: On the specification and verification of model transformations. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol. 5700, pp. 140–161. Springer, Heidelberg (2009)
Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. TOSEM 21(2), 13 (2012)
QVT (2005), http://www.omg.org/spec/QVT/1.0/PDF/ (last accessed November 2010)
Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)
Spivey, J.M.: An introduction to Z and formal specifications. Softw. Eng. J. 4(1), 40–50 (1989)
Steel, J., Jézéquel, J.-M.: On model ty**. SoSyM 6(4), 401–413 (2007)
Vallecillo, A., Gogolla, M.: Ty** model transformations using Tracts. In: Hu, Z., de Lara, J. (eds.) ICMT 2012. LNCS, vol. 7307, pp. 56–71. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Büttner, F., Egea, M., Guerra, E., de Lara, J. (2013). Checking Model Transformation Refinement. In: Duddy, K., Kappel, G. (eds) Theory and Practice of Model Transformations. ICMT 2013. Lecture Notes in Computer Science, vol 7909. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38883-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-38883-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38882-8
Online ISBN: 978-3-642-38883-5
eBook Packages: Computer ScienceComputer Science (R0)