Full contract verification for ATL using symbolic execution | Software and Systems Modeling Skip to main content
Springer Nature Link
Log in

Full contract verification for ATL using symbolic execution

  • Special Section Paper
  • Published:
Software & Systems Modeling Aims and scope Submit manuscript

Abstract

The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

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

Similar content being viewed by others

Notes

  1. We include ATL’s called rules under lazy rules.

  2. The logical connections between the contracts is not represented graphically.

  3. We here exclude rule reachability contracts, as the prover now automatically reports the failure of a rule to execute.

  4. AUTomotive Open System ARchitecture, www.AUTOSAR.org/.

  5. Related work concerning Tracts is discussed in more detail in Sect. 9.

  6. Note that this guidance is partially addressed in our work. When path conditions fail a contract, we report the path condition which represents the minimum number of rules. Therefore, it is the interaction of these rules that cause the contract to fail.

References

  1. A Short Introduction to SyVOLT. https://www.youtube.com/watch?v=8PrR5RhPptY

  2. ATL Zoo. http://www.eclipse.org/atl/atlTransformations

  3. ATL2DSLTrans Artifacts. http://msdl.cs.mcgill.ca/people/levi/files/MODELS2015_SoSyM

  4. Atlas Transformation Language (ATL). http://eclipse.org/atl

  5. Amrani, M., Lúcio, L., Selim, G.M.K., Combemale, B., Dingel, J., Vangheluwe, H., Traon, Y.L., Cordy, J.R.: A tridimensional approach for studying the formal verification of model transformations. In: Proceedings of ICSTW, pp. 921–928 (2012). doi:10.1109/ICST.2012.197

  6. Anastasakis, K., Bordbar, B., Küster, J.M.: Analysis of model transformations via alloy. In: Proceedings of MoDeVVa, pp. 47–56 (2007)

  7. Arendt, T., Habel, A., Radke, H., Taentzer, G.: From core OCL invariants to nested graph constraints. In: Proceedings of ICGT, 8571, pp. 97–112 (2014). doi:10.1007/978-3-319-09108-2_7

  8. Balogh, A., et al.: Workflow-driven tool integration using model transformations. In: Graph Transformations and Model-Driven Engineering, pp. 224–248 (2010)

  9. Barroca, B., Lúcio, L., Amaral, V., Félix, R., Sousa, V.: DSLTrans: a turing incomplete transformation language. In: Proceedings of SLE, pp. 296–305 (2011). doi:10.1007/978-3-642-19440-5_19

  10. Bergmann, G.: Translating OCL to graph patterns. In: Proceedings of MoDELS, 8767, pp. 670–686 (2014). doi:10.1007/978-3-319-11653-2_41

  11. Brambilla, M., Cabot, J., Wimmer, M.: Model-Driven Software Engineering in Practice. Morgan & Claypool Publishers, San Rafael (2012)

    Google Scholar 

  12. Burgueno, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Softw. Eng. 41(5), 490–506 (2015)

    Article  Google Scholar 

  13. Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ’off-the-shelf’ SMT solvers. In: Proceedings of MoDELS, pp. 432–448 (2012). doi:10.1007/978-3-642-33666-9_28

  14. Büttner, F., Egea, M., Guerra, E., De Lara, J.: Checking model transformation refinement. In: Proceedings of ICMT, pp. 158–173 (2013). doi:10.1007/978-3-642-38883-5_15

  15. Calegari, D., Luna, C., Szasz, N., Tasistro, A.: A type-theoretic framework for certified model transformations. In: Proceedings of SBMF, 6527, pp. 112–127 (2010). doi:10.1007/978-3-642-19829-8_8

  16. Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations. ECEASST 24, 1–15 (2009). doi:10.14279/tuj.eceasst.24.326

  17. Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: Proceedings of ICMT, pp. 133–148 (2015). doi:10.1007/978-3-319-21155-8_11

  18. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude–A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer, Berlin (2007)

    MATH  Google Scholar 

  19. Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: Proceedings of ISSRE, pp. 34–44 (2014). doi:10.1109/ISSRE.2014.10

  20. Gammaitoni, L., Kelsen, P.: F-alloy: an alloy based model transformation language. In: Proceedings of ICMT, pp. 166–180 (2015). doi:10.1007/978-3-319-21155-8_13

  21. García-Domínguez, A., Kolovos, D.S., Rose, L.M., Paige, R.F., Medina-Bulo, I.: EUnit: a unit testing framework for model management tasks. In: Proceedings of MoDELS, pp. 395–409 (2011). doi:10.1007/978-3-642-24485-8_29

  22. Giner, P., Pelechano, V.: Test-driven development of model transformations. In: Proceedings of MoDELS, pp. 748–752 (2009). doi:10.1007/978-3-642-04425-0_61

  23. Gogolla, M., Hamann, L., Hilken, F.: Checking transformation model properties with a UML and OCL model validator. In: Proceedings of VOLT, pp. 16–25 (2014)

  24. Gogolla, M., Vallecillo, A.: Tractable model transformation testing. In: Proceedings of ECMFA, pp. 221–235 (2011). doi:10.1007/978-3-642-21470-7_16

  25. González, C.A., Cabot, J.: ATLTest: a white-box test generation approach for ATL transformations. In: Proceedings of MoDELS, pp. 449–464 (2012). doi:10.1007/978-3-642-33666-9_29

  26. 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). doi:10.1007/s10515-012-0102-y

    Article  Google Scholar 

  27. Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1–2), 31–39 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  28. Kolovos, D.S., Paige, R.F., Polack, F.A.: Model comparison: a foundation for model composition and model transformation testing. In: Proceedings of GaMMa, pp. 13–20 (2006). doi:10.1145/1138304.1138308

  29. Lano, K., Clark, T., Rahimi, S.K.: A framework for model transformation verification. Formal Asp. Comput. 27(1), 193–235 (2015). doi:10.1007/s00165-014-0313-z

    Article  MathSciNet  MATH  Google Scholar 

  30. Lúcio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: Proceedings of MoDELS, pp. 136–150 (2010). doi:10.1007/978-3-642-16145-2_10

  31. Lúcio, L., Oakes, B., Vangheluwe, H.: A Technique for Symbolically Verifying Properties of Graph-based Model Transformations. Technical report SOCS-TR-2014.1, McGill University (2014)

  32. Lúcio, L., Oakes, B.J., Gomes, C., Selim, G.M., Dingel, J., Cordy, J.R., Vangheluwe, H.: SyVOLT: Full model transformation verification using contracts. In: Proceedings of MoDELS 2015 Demo and Poster Session, pp. 24–27 (2015)

  33. Lúcio, L., Amrani, M., Dingel, J., Lambers, L., Salay, R., Selim, G., Syriani, E., Wimmer, M.: Model transformation intents and their properties. Softw. Syst. Model., pp. 1–38 (2014). doi:10.1007/s10270-014-0429-x

  34. Mottu, J.M., Baudry, B., Traon, Y.L.: Model transformation testing: oracle issue. In: Proceedings of ICSTW, pp. 105–112 (2008). doi:10.1109/icstw.2008.27

  35. Oakes, B.J., Troya, J., Lúcio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: Proceedings of MoDELS, pp. 256–265 (2015). doi:10.1109/models.2015.7338256

  36. Paen, E.: Measuring Incrementally Developed Model Transformations Using Change Metrics. Master’s thesis, Queen’s University (2012)

  37. Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in coq. In: Proceedings of ICFEM, pp. 56–73 (2010). doi:10.1007/978-3-642-16901-4_6

  38. Posse, E., Dingel, J.: An executable formal semantics for UML-RT. Softw. Syst. Model. 15(1), 179–217 (2016). doi:10.1007/s10270-014-0399-z

    Article  Google Scholar 

  39. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015). doi:10.1007/s10270-013-0358-0

    Article  Google Scholar 

  40. Richa, E., Borde, E., Pautet, L.: Translating ATL model transformations to algebraic graph transformations. In: Proceedings of ICMT, pp. 183–198 (2015). doi:10.1007/978-3-319-21155-8_14

  41. Selim, G.M.: Formal Verification of Graph-Based Model Transformations. Ph.D. thesis, Queen’s University (2015)

  42. Selim, G.M., Cordy, J.R., Dingel, J., Lúcio, L., Oakes, B.J.: Finding and fixing bugs in model transformations with formal verification: an experience report. In: Proceedings of AMT, pp. 26–35 (2015)

  43. Selim, G.M., Lúcio, L., Cordy, J.R., Dingel, J., Oakes, B.J.: Specification and verification of graph-based model transformation properties. In: Proceedings of ICGT, pp. 113–129 (2014). doi:10.1007/978-3-319-09108-2_8

  44. Syriani, E., Vangheluwe, H., LaShomb, B.: T-Core: a framework for custom-built model transformation engines. Softw. Syst. Model. 14(3), 1215–1243 (2015). doi:10.1007/s10270-013-0370-4

    Article  Google Scholar 

  45. SyVOLT tool. http://msdl.cs.mcgill.ca/people/levi/contractprover

  46. Tisi, M., Martínez, S., Jouault, F., Cabot, J.: Refining Models with Rule-based Model Transformations. Research report RR-7582, INRIA (2011)

  47. Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. J. Object Technol. 10(5), 1–29 (2011). doi:10.5381/jot.2011.10.1.a5

    Google Scholar 

  48. Vallecillo, A., Gogolla, M., Burgueno, L., Wimmer, M., Hamann, L.: Formal specification and testing of model transformations. In: Formal Methods for Model-Driven Engineering, pp. 399–437 (2012)

  49. Wieber, M., Anjorin, A., Schürr, A.: On the usage of TGGs for automated model transformation testing. In: Proceedings of ICMT, pp. 1–16 (2014)

Download references

Acknowledgments

The authors warmly thank Gehan Selim and Cláudio Gomes for their contributions to the implementation of the contract prover. Bentley James Oakes is funded by an NSERC grant, as well as support from the NECSIS project, funded by Automotive Partnership, Canada. The work of Javier Troya is funded by the European Commission (FEDER) and the Spanish and the Andalusian R&D&I programmes under grants and projects BELI (TIN2015-70560-R), THEOS (P10-TIC-5906), and COPAS (P12-TIC-1867). Finally, the work of Manuel Wimmer is funded by the Christian Doppler Forschungsgesellschaft and the BMWFW, Austria.

Author information

Authors and Affiliations

  1. School of Computer Science, McGill University, Montreal, Canada

    Bentley James Oakes

  2. Department of Computing Languages and Systems, University of Seville, Seville, Spain

    Javier Troya

  3. fortiss GmbH, Munich, Germany

    Levi Lúcio

  4. Business Informatics Group, TU Wien, Vienna, Austria

    Manuel Wimmer

Authors
  1. Bentley James Oakes
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. Javier Troya
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. Levi Lúcio
    View author publications

    You can also search for this author inPubMed Google Scholar

  4. Manuel Wimmer
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Bentley James Oakes.

Additional information

Communicated by Jordi Cabot and Alexander Egyed.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Oakes, B.J., Troya, J., Lúcio, L. et al. Full contract verification for ATL using symbolic execution. Softw Syst Model 17, 815–849 (2018). https://doi.org/10.1007/s10270-016-0548-7

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10270-016-0548-7

Keywords