Skip to main content
SpringerLink
Log in

Automated verification of model transformations based on visual contracts

  • Published:
Automated Software Engineering Aims and scope Submit manuscript

Abstract

Model-Driven Engineering promotes the use of models to conduct the different phases of the software development. In this way, models are transformed between different languages and notations until code is generated for the final application. Hence, the construction of correct Model-to-Model (M2M) transformations becomes a crucial aspect in this approach.

Even though many languages and tools have been proposed to build and execute M2M transformations, there is scarce support to specify correctness requirements for such transformations in an implementation-independent way, i.e., irrespective of the actual transformation language used.

In this paper we fill this gap by proposing a declarative language for the specification of visual contracts, enabling the verification of transformations defined with any transformation language. The verification is performed by compiling the contracts into QVT to detect disconformities of transformation results with respect to the contracts. As a proof of concept, we also report on a graphical modeling environment for the specification of contracts, and on its use for the verification of transformations in several case studies.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20
Fig. 21
Fig. 22
Fig. 23
Fig. 24
Fig. 25
Fig. 26
Fig. 27
Fig. 28
Fig. 29
Fig. 30
Fig. 31
Fig. 32
Fig. 33
Fig. 34
Fig. 35
Fig. 36
Fig. 37
Fig. 38
Fig. 39
Fig. 40
Fig. 41

Similar content being viewed by others

References

  • Aranega, V., Mottu, J.-M., Etien, A., Dekeyser, J.-L.: Using trace to situate errors in model transformations. In: Software and Data Technologies. Communications in Computer and Information Science, vol. 50, pp. 137–149. Springer, Berlin (2011)

    Chapter  Google Scholar 

  • Balogh, A., Bergmann, G., Csertán, G., Gönczy, L., Horváth, A., Majzik, I., Pataricza, A., Polgár, B., Ráth, I., Varró, D., Varró, G.: Workflow-driven tool integration using model transformations. In: Graph Transformations and Model-Driven Engineering. LNCS, vol. 5765, pp. 224–248. Springer, Berlin (2010)

    Chapter  Google Scholar 

  • Baudry, B., Dinh-Trong, T., Mottu, J., Simmonds, D., France, R., Ghosh, S., Fleurey, F., Le Traon, Y.: Model transformation testing challenges. In: ECMDA Workshop on Integration of Model Driven Development and Model Driven Testing, vol. 92 (2006)

    Google Scholar 

  • Baudry, B., Ghosh, S., Fleurey, F., France, R., Le Traon, Y., Mottu, J.-M.: Barriers to systematic model transformation testing. Commun. ACM 53, 139–143 (2010)

    Article  Google Scholar 

  • Beugnard, A., Jézéquel, J.-M., Plouzeau, N., Watkins, D.: Making components contract aware. Computer 32, 38–45 (1999)

    Article  Google Scholar 

  • Bézivin, J.: On the unification power of models. Softw. Syst. Model. 4(2), 31 (2005)

    Article  Google Scholar 

  • Bézivin, J., Rumpe, B., Schürr, A., Tratt, L.: Model transformations in practice. In: Workshop of MoDELS’05 (2005)

    Google Scholar 

  • Briand, L.C., Labiche, Y., Sun, H.: Investigating the use of analysis contracts to improve the testability of object-oriented code. Softw. Pract. Exp. 33(7), 637–672 (2003)

    Article  MATH  Google Scholar 

  • Brottier, E., Fleurey, F., Steel, J., Baudry, B., Traon, Y.L.: Metamodel-based test generation for model transformations: an algorithm and a tool. In: ISSRE’06, pp. 85–94. IEEE Comput. Soc., Los Alamitos (2006)

    Google Scholar 

  • 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)

    Article  Google Scholar 

  • Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: Workshop on OCL and Model Driven Engineering UML’04, vol. 12, pp. 69–83 (2004)

    Google Scholar 

  • Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations. In: ECEASST, vol. 24 (2009)

    Google Scholar 

  • Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J. 45(3), 621–645 (2006)

    Article  Google Scholar 

  • EMF: Eclipse Modeling Framework. www.eclipse.org/emf. Last accessed: January 2012

  • Fishman, G.S.: Discrete-Event Simulation: Modeling, Programming, and Analysis. Springer, Berlin (2001)

    MATH  Google Scholar 

  • Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: testing model transformations. In: MoDeVa’04, pp. 29–40. IEEE Comput. Soc., Los Alamitos (2004)

    Google Scholar 

  • Fleurey, F., Baudry, B., Muller, P.-A., Traon, Y.: Qualifying input test data for model transformations. Softw. Syst. Model. 8, 185–203 (2009)

    Article  Google Scholar 

  • France, R., Rumpe, B.: Model-driven development of complex software: A research roadmap. In: FOSE’07, pp. 37–54. IEEE Comput. Soc., Los Alamitos (2007)

    Google Scholar 

  • Giner, P., Pelechano, V.: Test-driven development of model transformations. In: MODELS’09. LNCS, vol. 5795, pp. 748–752. Springer, Berlin (2009)

    Google Scholar 

  • Gogolla, M., Vallecillo, A.: Tractable model transformation testing. In: ECMFA’11. LNCS, vol. 6698, pp. 221–235. Springer, Berlin (2011)

    Google Scholar 

  • Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley Professional, Reading (2009). See also http://www.eclipse.org/modeling/gmp/

    Google Scholar 

  • Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F.: A visual specification language for model-to-model transformations. In: VL/HCC, pp. 119–126. IEEE Comput. Soc., Los Alamitos (2010)

    Google Scholar 

  • Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F., dos Santos, O.M.: Engineering model transformations with transML. Softw. Syst. Mod. (2011, in press). doi:10.1007/s10270-011-0211-2

  • Jackson, D.: Software Abstractions. Logic, Language, and Analysis. MIT Press, Cambridge (2006)

    Google Scholar 

  • Jensen, K.: Coloured Petri Nets Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science. Springer, Berlin (1997)

    MATH  Google Scholar 

  • Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3–4), 213–254 (2007)

    Article  Google Scholar 

  • Jouault, F., Kurtev, I.: Transforming models with ATL. In: Model Transformations in Practice Workshop (2005)

    Google Scholar 

  • Kessentini, M., Sahraoui, H.A., Boukadoum, M.: Example-based model-transformation testing. Autom. Softw. Eng. 18(2), 199–224 (2011)

    Article  Google Scholar 

  • Kolovos, D., Paige, R., Polack, F.: The Epsilon transformation language. In: ICMT’08. LNCS, vol. 5063, pp. 46–60. Springer, Berlin (2008a)

    Google Scholar 

  • Kolovos, D., Paige, R., Rose, L., Polack, F.: Unit testing model management operations. In: ICSTW’08, pp. 97–104. IEEE Comput. Soc., Los Alamitos (2008b)

    Google Scholar 

  • Kolovos, D.S., Paige, R.F., Polack, F.A.: Model comparison: a foundation for model composition and model transformation testing. In: GaMMa’06, pp. 13–20. ACM Press, New York (2006)

    Google Scholar 

  • Kühne, T.: Matters of (meta-)modeling. Softw. Syst. Model. 5(4), 369–385 (2006)

    Article  Google Scholar 

  • Küster, J.M.: Definition and validation of model transformations. Softw. Syst. Model. 5(3), 233–259 (2006)

    Article  Google Scholar 

  • Küster, J.M., Abd-El-Razik, M.: Validation of model transformations—first experiences using a white box approach. In: Models in Software Engineering. LNCS, vol. 4364, pp. 193–204. Springer, Berlin (2006)

    Chapter  Google Scholar 

  • Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1–3), 185–208 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  • Lin, Y., Zhang, J., Gray, J.: Model comparison: A key challenge for transformation testing and version control in model driven software development. In: OOPSLA Workshop on Best Practices for Model-Driven Software Development (2004)

    Google Scholar 

  • Lin, Y., Zhang, J., Gray, J.: A testing framework for model transformations. In: Model-Driven Software Development, pp. 219–236 (2005)

    Chapter  Google Scholar 

  • Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125–142 (2006)

    Article  Google Scholar 

  • Meyer, B.: Applying “design by contract”. Computer 25, 40–51 (1992)

    Article  Google Scholar 

  • Mottu, J.-M., Baudry, B., Le Traon, Y.: Reusable MDA components: A testing-for-trust approach. In: MoDELS’06. LNCS, vol. 4199, pp. 589–603. Springer, Berlin (2006)

    Google Scholar 

  • Mottu, J.-M., Baudry, B., Traon, Y.L.: Model transformation testing: oracle issue. In: ICSTW’08, pp. 105–112. IEEE Comput. Soc., Los Alamitos (2008)

    Google Scholar 

  • Object Management Group: OCL Specification Version 2.0. http://www.omg.org/docs/ptc/05-06-06.pdf, 2005

  • Object Management Group: QVT Specification Version 1.1. http://www.omg.org/spec/QVT/1.1/, 2011

  • Ramos, R., Barais, O., Jézéquel, J.-M.: Matching model-snippets. In: MoDELS’07. LNCS, vol. 4735, pp. 121–135. Springer, Berlin (2007)

    Google Scholar 

  • Schmidt, D.C.: Model-driven engineering. Computer 39(2), 25–31 (2006)

    Article  Google Scholar 

  • Sen, S., Baudry, B., Mottu, J.-M.: Automatic model generation strategies for model transformation testing. In: ICMT’09. LNCS, vol. 5563, pp. 148–164. Springer, Berlin (2009)

    Google Scholar 

  • Spivey, J.M.: An introduction to Z and formal specifications. Softw. Eng. J. 4(1), 40–50 (1989)

    Article  Google Scholar 

  • TATA Research Development and Design: ModelMorf. http://www.tcs-trddc.com/trddc_website/ModelMorf/ModelMorf.htm. Last accessed: January 2012

  • Traon, Y.L., Baudry, B., Jézéquel, J.-M.: Design by contract to improve software vigilance. IEEE Trans. Softw. Eng. 32(8), 571–586 (2006)

    Article  Google Scholar 

  • Varró, D., Varró-Gyapay, S., Ehrig, H., Prange, U., Taentzer, G.: Termination analysis of model transformations by Petri nets. In: ICGT’06. LNCS, vol. 4178, pp. 260–274. Springer, Berlin (2006)

    Google Scholar 

  • Xpand: Xpand Templates. http://wiki.eclipse.org/Xpand. Last accessed: January 2012

Download references

Author information

Authors and Affiliations

  1. Universidad Autónoma de Madrid, Madrid, Spain

    Esther Guerra & Juan de Lara

  2. Vienna University of Technology, Vienna, Austria

    Manuel Wimmer, Gerti Kappel & Johannes Schönböck

  3. Johannes Kepler University Linz, Linz, Austria

    Angelika Kusel, Werner Retschitzegger & Wieland Schwinger

Authors
  1. Esther Guerra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Juan de Lara
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Manuel Wimmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gerti Kappel
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Angelika Kusel
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Werner Retschitzegger
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Johannes Schönböck
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Wieland Schwinger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Esther Guerra.

Additional information

This work has been funded by the Austrian Science Fund (FWF) under grant P21374-N13, the Spanish Ministry of Science under grants TIN2008-02081 and TIN2011-24139, and the R&D programme of the Madrid Region under project S2009/TIC-1650.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Guerra, E., de Lara, J., Wimmer, M. et al. Automated verification of model transformations based on visual contracts. Autom Softw Eng 20, 5–46 (2013). https://doi.org/10.1007/s10515-012-0102-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10515-012-0102-y

Keywords

Search

Navigation