A Deductive Approach for Fault Localization in ATL Model Transformations

  • Zheng ChengEmail author
  • Massimo Tisi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


In model-driven engineering, correct model transformation is essential for reliably producing the artifacts that drive software development. While the correctness of a model transformation can be specified and checked via contracts, debugging unverified contracts imposes a heavy cognitive load on transformation developers. To improve this situation, we present an automatic fault localization approach, based on natural deduction, for the ATL model transformation language. We start by designing sound natural deduction rules for the ATL language. Then, we propose an automated proof strategy that applies the designed deduction rules on the postconditions of the model transformation to generate sub-goals: successfully proving the sub-goals implies the satisfaction of the postconditions. When a sub-goal is not verified, we present the user with sliced ATL model transformation and predicates deduced from the postcondition as debugging clues. We provide an automated tool that implements this process. We evaluate its practical applicability using mutation analysis, and identify its limitations.


Model Transformation Fault Localization Natural Deduction Satisfiability Modulo Theory Proof Strategy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    A deductive approach for fault localization in ATL model transformations (2016).
  2. 2.
    Ab. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)Google Scholar
  3. 3.
    Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRefGoogle Scholar
  4. 4.
    Aranega, V., Mottu, J., Etien, A., Dekeyser, J.: Traceability mechanism for error localization in model transformation. In: 4th International Conference on Software and Data Technologies, Sofia, Bulgaria, pp. 66–73 (2009)Google Scholar
  5. 5.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi: 10.1007/11804192_17 CrossRefGoogle Scholar
  6. 6.
    Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and esterel. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 2–2. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-79707-4_2 CrossRefGoogle Scholar
  7. 7.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)zbMATHGoogle Scholar
  8. 8.
    Burgueño, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Softw. Eng. 41(5), 490–506 (2015)CrossRefGoogle Scholar
  9. 9.
    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). doi: 10.1007/978-3-642-33666-9_28 CrossRefGoogle Scholar
  10. 10.
    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). doi: 10.1007/978-3-642-34281-3_16 CrossRefGoogle Scholar
  11. 11.
    Calegari, D., Luna, C., Szasz, N., Tasistro, Á.: A type-theoretic framework for certified model transformations. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 112–127. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-19829-8_8 CrossRefGoogle Scholar
  12. 12.
    Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: Kolovos, D., Wimmer, M. (eds.) ICMT 2015. LNCS, vol. 9152, pp. 133–148. Springer, Cham (2015). doi: 10.1007/978-3-319-21155-8_11 CrossRefGoogle Scholar
  13. 13.
    Combemale, B., Crégut, X., Garoche, P., Thirioux, X.: Essay on semantics definition in MDE - an instrumented approach for model verification. J. Softw. 4(9), 943–958 (2009)CrossRefGoogle Scholar
  14. 14.
    Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: 25th IEEE International Symposium on Software Reliability Engineering, pp. 34–44. IEEE, Naples (2014)Google Scholar
  15. 15.
    Filliâtre, J.-C., Paskevich, A.: Why3 — Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37036-6_8 CrossRefGoogle Scholar
  16. 16.
    Huth, M., Ryan, M.: Logic in Computer Science Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)CrossRefzbMATHGoogle Scholar
  17. 17.
    Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRefGoogle Scholar
  18. 18.
    Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: A model transformation tool. Sci. Comput. Program. 72(1–2), 31–39 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193–235 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  21. 21.
    Oakes, B.J., Troya, J., Lúcio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 256–265. IEEE, Ottawa (2015)Google Scholar
  22. 22.
    Object Management Group: The Object Constraint Language Specification (ver. 2.0) (2006).
  23. 23.
    Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in Coq. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 56–73. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-16901-4_6 CrossRefGoogle Scholar
  24. 24.
    Roychoudhury, A., Chandra, S.: Formula-based software debugging. Commun. ACM 59(7), 68–77 (2016)CrossRefGoogle Scholar
  25. 25.
    Selim, G.M.K., Wang, S., Cordy, J.R., Dingel, J.: Model transformations for migrating legacy models: an industrial case study. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., Störrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 90–101. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31491-9_9 CrossRefGoogle Scholar
  26. 26.
    Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework, 2nd edn. Pearson Education, London (2008)Google Scholar
  27. 27.
    Tip, F.: A survey of program slicing techniques. Technical report, Centrum Wiskunde & Informatica (1994)Google Scholar
  28. 28.
    Tisi, M., Martínez, S., Choura, H.: Parallel execution of ATL transformation rules. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 656–672. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-41533-3_40 CrossRefGoogle Scholar
  29. 29.
    Wagelaar, D.: Using ATL/EMFTVM for import/export of medical data. In: 2nd Software Development Automation Conference, Amsterdam, Netherlands (2014)Google Scholar
  30. 30.
    Weiser, M.: Program slicing. In: 5th International Conference on Software Engineering, pp. 439–449. IEEE, New Jersey (1981)Google Scholar
  31. 31.
    Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. Pre-Print (99), 1–41 (2016)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.AtlanMod Team (Inria, IMT Atlantique, LS2N)NantesFrance

Personalised recommendations