Skip to main content
SpringerLink
Log in

Formalised EMFTVM bytecode language for sound verification of model transformations

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

Abstract

Model-driven engineering is an effective approach for addressing the full life cycle of software development. Model transformation is widely acknowledged as one of its central ingredients. With the increasing complexity of model transformations, it is urgent to develop verification tools that prevent incorrect transformations from generating faulty models. However, the development of sound verification tools is a non-trivial task, due to unimplementable or erroneous execution semantics encoded for the target model transformation language. In this work, we develop a formalisation for the EMFTVM bytecode language by using the Boogie intermediate verification language. It ensures the model transformation language has an implementable execution semantics by reliably prototyping the implementation of the model transformation language. It also ensures the absence of erroneous execution semantics encoded for the target model transformation language by using a translation validation approach.

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

Similar content being viewed by others

Notes

  1. Notice that when the ATL transformation is compiled into an EMFTVM implementation, the second binding always overwrites the first binding (Sect. 6.3).

  2. EMFTVM bytecode format. https://wiki.eclipse.org/ATL/EMFTVM.

  3. When more than one target element is generated by y, then the first target element generated by y is returned. For example, assuming y is processed by a rule with the format: \(\mathbf{rule }\, r\{\mathbf{from }\, y:Y\, \mathbf{to }\, n:N,\, m:M\}\), then the n generated for y will be returned.

  4. For simplicity, we do not consider the inheritance of transformation rules [69].

  5. We count each generated Boogie procedure/implementation pair as a verification task.

References

  1. Amrani, M., Lucio, L., Selim, G., Combemale, B., Dingel, J., Vangheluwe, H., Le Traon, Y., Cordy, J.R.: A tridimensional approach for studying the formal verification of model transformations. In: 5th International Conference on Software Testing, Verification and Validation. pp. 921–928. IEEE, Washington, DC, USA (2012)

  2. Anastasakis, K., Bordbar, B., Küster., J.M.: Analysis of model transformations via Alloy. In: 4th Workshop on Model-Driven Engineering, Verification and Validation. pp. 47–56. Nashville, TN, USA (2007)

  3. Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: 13th International Conference on Model Driven Engineering Languages and Systems, pp. 121–135. Springer, Oslo, Norway (2010)

  4. Asztalos, M., Lengyel, L., Levendovszky, T.: Formal specification and analysis of functional properties of graph rewriting-based model transformation. Softw. Test. Verif. Reliab. 23(5), 405–435 (2013)

    Article  Google Scholar 

  5. ATLAS Group: Specification of the ATL virtual machine. Tech. rep., Lina & INRIA Nantes (2005)

  6. Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: 4th International Conference on Formal Methods for Components and Objects, pp. 364–387. Springer, Amsterdam, Netherlands (2006)

  7. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: 1st International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 49–69. Springer, Marseille, France (2005)

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

    Article  Google Scholar 

  9. Benelellam, A., Gomez-Llana, A., Tisi, M., Cabot, J.: Distributed model-to-model transformation with ATL on MapReduce. In: 8th International Conference on Software Language Engineering, pp. 37–48. ACM, Pittsburg, USA (2015)

  10. Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: 12th International Workshop on Formal Methods for Industrial Critical Systems, pp. 2–2. Springer, Berlin, Germany (2008)

  11. Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing, Birmingham (2013)

    Google Scholar 

  12. Bock, C., Cook, S., Rivett, P., Rutt, T., Seidewitz, E., Selic, B., Tolbert, D.: OMG Unified Modeling Language (ver. 2.5). Tech. Rep. formal/2015-03-01 (2015)

  13. Bornat, R.: Proving pointer programs in Hoare logic. In: International Conference on Mathematics of Program Construction, pp. 102–126. Springer, Ponte de Lima, Portugal (2000)

  14. Burgueño, 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 

  15. Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: 14th International Conference on Formal Engineering Methods, pp. 198–213. Springer, Kyoto, Japan (2012)

  16. Calegari, D., Luna, C., Szasz, N., Tasistro, Á.: A type-theoretic framework for certified model transformations. In: 13th Brazilian Symposium on Formal Methods, pp. 112–127. Springer, Natal, Brazil (2011)

  17. Calegari, D., Szasz, N.: Verification of model transformations: a survey of the state-of-the-art. Electron. Notes in Theor. Comput. Sci. 292, 5–25 (2013)

    Article  Google Scholar 

  18. Chan, K.: Formal proofs for QoS-oriented transformations. In: 10th International Conference Workshops on Enterprise Distributed Object Computing, pp. 41–41. IEEE, Hong Kong, China (2006)

  19. Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: 8th International Conference on Model Transformation, pp. 133–148. Springer, L’Aquila, Italy (2015)

  20. Cheng, Z., Monahan, R., Power, J.F.: Online repository for formalised EMFTVM bytecode language. https://github.com/veriatl/Compiler.Emftvm2Boogie (2016)

  21. Cheng, Z.: Formal Verification of Relational Model Transformations Using an Intermediate Verification Language. Ph.D. thesis, Maynooth University (2016)

  22. 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)

    Article  Google Scholar 

  23. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM, Los Angeles, California (1977)

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

    Article  Google Scholar 

  25. Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: 31st International Conference on Software Engineering, pp. 429–430. IEEE, Vancouver, British Columbia (2009)

  26. Darvas, Á., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: 10th International Conference on Fundamental Approaches to Software Engineering, pp. 336–351. Springer, Braga, Portugal (2007)

  27. Darvas, Á., Müller, P.: Reasoning about method calls in interface specifications. J. Object Technol. 5(5), 59–85 (2006)

    Article  Google Scholar 

  28. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer, Budapest, Hungary (2008)

  29. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  30. Filliâtre, J.C., Paskevich, A.: Why3— where programs meet provers. In: 22nd European Symposium on Programming, pp. 125–128. Springer, Rome, Italy (2013)

  31. Filliâtre, J.C.: Why: A multi-language multi-prover verification tool. Tech. rep., Université Paris Sud (2003)

  32. Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1–2), 101–122 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  33. Guerra, E., de Lara, J.: Colouring: execution, debug and analysis of QVT-relations transformations through coloured Petri nets. Softw. Syst. Model. 13(4), 1447–1472 (2014)

    Article  Google Scholar 

  34. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  35. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  36. Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 653–667. Springer, Wellington, New Zealand (2011)

  37. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)

    Article  Google Scholar 

  38. Jouault, F.: The resolve algorithm implemented in the ASM language. http://git.eclipse.org/c/mmt/org.eclipse.atl.git/tree/dsls/ATL/Compiler/ATL.acg (2007)

  39. 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 

  40. Klatt, B.: Xpand: a closer look at the model2text transformation language. http://bar54.de/benjamin.klatt-xpand.pdf (2007)

  41. Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman, Boston (2003)

    Google Scholar 

  42. Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193–235 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  43. Lehner, H., Müller, P.: Formal translation of bytecode into BoogiePL. In: 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformation, pp. 35–50. Elsevier, Budapest, Hungary (2007)

  44. Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. In: 12th International Conference on Fundamental Approaches to Software Engineering, pp. 231–245. Springer, York, UK (2009)

  45. Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: 24th Annual ACM Symposium on Applied Computing, pp. 615–622. ACM, Hawaii, USA (2009)

  46. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348–370. Springer, Dakar, Senegal (2010)

  47. Leino, K.R.M.: This is Boogie 2. http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf. Microsoft Research, Redmond, USA (2008)

  48. Lúcio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: 13th International Conference on Model Driven Engineering Languages and Systems, pp. 136–150. Springer, Oslo, Norway (2010)

  49. Lúcio, L., Vangheluwe, H.: Model transformations to verify model transformations. In: 2nd Workshop on Verification of Model Transformations. Budapest, Hungary (2013)

  50. Manna, Z., McCarthy, J.: Properties of programs and partial function logic. Mach. Intell. 5, 27–38 (1969)

    MATH  Google Scholar 

  51. Mottu, J., Baudry, B., Traon, Y.L.: Mutation analysis testing for model transformations. In: 2nd European Conference on Model Driven Architecture-Foundations and Applications. pp. 376–390. Springer, Bilbao, Spain (2006)

  52. Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 151–166. Springer, London, UK (1998)

  53. Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in Coq. In: 12th International Conference on Formal Engineering Methods, pp. 56–73. Springer, Shanghai, China (2010)

  54. Poernomo, I.: Proofs-as-model-transformations. In: 1st International Conference on Model Transformation, pp. 214–228. Springer, Zürich, Switzerland (2008)

  55. Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)

    Article  Google Scholar 

  56. Sahin, D., Kessentini, M., Wimmer, M., Deb, K.: Model transformation testing: a bi-level search-based software engineering approach. J. Softw. Evol. Process 27(11), 821–837 (2015)

    Article  Google Scholar 

  57. Schätz, B.: Verification of model transformations. In: 9th International Workshop on Graph Transformation and Visual Modeling Techniques, pp. 130–142. EASST, Paphos, Cyprus (2010)

  58. Selim, G., Wang, S., Cordy, J., Dingel, J.: Model transformations for migrating legacy models: an industrial case study. In: 8th European Conference on Modelling Foundations and Applications, pp. 90–101. Springer, Lyngby, Denmark (2012)

  59. Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: eclipse modeling framework, 2nd edn. Pearson Education, London (2008)

    Google Scholar 

  60. Syriani, E., Vangheluwe, H.: A modular timed graph transformation language for simulation-based design. Softw. Syst. Model. 12(2), 387–414 (2013)

    Article  Google Scholar 

  61. Tristan, J., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 295–305. ACM, San Jose, USA (2011)

  62. Tristan, J., Leroy, X.: A simple, verified validator for software pipelining. In: 37th ACM Symposium on Principles of Programming Languages, pp. 83–92. ACM, Madrid, Spain (2010)

  63. Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. J. Object Technol. 10(5), 1–29 (2011)

    Google Scholar 

  64. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: Computing Research Repository abs/1106.4700 (2011)

  65. Varró, G., Varró, D., Friedl, K.: Adaptive graph pattern matching for model transformations using model-sensitive search plans. In: 1st International Workshop on Graph and Model Transformations, pp. 191–205. Elsevier, Brighton, United Kingdom (2006)

  66. Vépa, É., Bézivin, J., Brunelière, H., Jouault, F.: Measuring model repositories. In: Summary of the 2006 Model Size Metrics Workshop. Springer, Genoa, Italy (2006)

  67. Vignaga, A.: Metrics for measuring ATL model transformations. Tech. rep., Universidad de Chile (2009)

  68. Wagelaar, D., Iovino, L., Ruscio, D.D., Pierantonio, A.: Translational semantics of a co-evolution specific language with the EMF transformation virtual machine. In: 5th International Conference on Model Transformation, pp. 192–207. Springer, Prague, Czech Republic (2012)

  69. Wagelaar, D., Tisi, M., Cabot, J., Jouault, F.: Towards a general composition semantics for rule-based model transformation. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 623–637. Springer, Wellington, New Zealand (2011)

  70. Wagelaar, D.: The resolve algorithm implemented in the EMFTVM language. http://git.eclipse.org/c/mmt/org.eclipse.atl.git/tree/plugins/org.eclipse.m2m.atl.emftvm/src/org/eclipse/m2m/atl/emftvm/util/OCLOperations.java (2011)

  71. Wagelaar, D.: Using ATL/EMFTVM for import/export of medical data. In: 2nd Software Development Automation Conference. Amsterdam, Netherlands (2014)

  72. Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Schoenboeck, J., Schwinger, W.: Right or wrong? Verification of model transformations using colored Petri nets. In: 9th OOPSLA Workshop on Domain-Specific Modeling, pp. 101–106. Helsinki School of Economics, Orlando, USA (2009)

  73. Wu, H., Monahan, R., Power, J.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: 7th International Symposium on Theoretical Aspects of Software Engineering, pp. 175–182. IEEE, Birmingham, UK (2013)

Download references

Acknowledgments

Zheng Cheng is funded by the Doctoral Teaching scholarship and John & Pat Hume scholarship from Maynooth University and the MONDO (EU ICT-611125) Project. We thank the reviewers for their feedback to improve the representation of this submission.

Author information

Authors and Affiliations

  1. Department of Computer Science, Maynooth University, Maynooth, Co. Kildare, Ireland

    Zheng Cheng, Rosemary Monahan & James F. Power

Authors
  1. Zheng Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rosemary Monahan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. James F. Power
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zheng Cheng.

Additional information

Communicated by Prof. Alfonso Pierantonio.

Appendix: The translational semantics of EMFTVM bytecode language

Appendix: The translational semantics of EMFTVM bytecode language

In this section, we illustrate the translational semantics of the EMFTVM bytecode language in more detail. Overall, 42 out of 48 instructions are encoded by our formalisation for the EMFTVM bytecode language. The 6 EMFTVM instructions that are not encoded are omitted because of some technical limitations of our approach (e.g. transitive closure cannot be described in FOL [36]).

Table 3 Auxiliary notations used by the translational semantics of EMFTVM bytecode language
Full size table
Table 4 Translational semantics for EMFTVM stack handling instructions
Full size table
Table 5 Translational semantics for EMFTVM control flow instructions
Full size table

Some of the conventions we use are:

  • In general, we draw on the let..in expression to improve the readability of our formalisation. However, this is not a standard syntax in Boogie.

  • We use the superscript \(^\#\) to denote the line number of an EMFTVM instruction. This superscript is attached to the declared Boogie variables to avoid name collision.

  • We also use the notation of \(\llbracket \) S \(\rrbracket \)to represent the transformation from the EMFTVM construct S to its corresponding Boogie code.

In addition to our general encoding convention, the auxiliary notations used by our formalisation for stack, collection, heap, method invocation and metamodel are explained in Table 3.

Table 6 Translational semantics for EMFTVM model handling instructions
Full size table

The full translational semantics of the EMFTVM language is given in Tables 4, 5 and 6, classified by the category that each EMFTVM instruction resides in.

In general, our formalisation for the EMFTVM bytecode language is based on two main data structures (Sect. 3.1): the operand stack stk and the global memory model heap. We further introduce an access table acc to prohibit runtime exceptions caused by certain operations on the structural features (Sect. 3.4). Thus, checking whether o.f is set or not becomes an expression isset(acc, o, f). Marking o.f as set or not uses the expression set(acc, o, f, v).

In addition to the discussion of our formalisation for the EMFTVM bytecode language in Sect. 3, we explain six additional points:

  1. 1.

    In Table 4, the operational semantics of the GET_CB instruction is to push the code block Stmt onto the operand stack. It usually works with the INVOKE_CB_S instruction (Table 5), whose operational semantics is to execute the code block that is on top of the operand stack. Thus, in the translation rule for the GET_CB instruction, we introduce a fresh label (denoted by LABEL) to identify the translated EMFTVM code block, which is referred by the translation rule for the INVOKE_CB_S instruction.

  2. 2.

    In Table 5, to make sure the offset of the GOTO, IF and IFN instructions is valid in their corresponding translation rules, we insert a fresh Boogie label, denoted by \(\llbracket \)n\(\rrbracket \), at the program point which corresponds to the offset n of these instructions (Sect. 3.3).

  3. 3.

    In Table 5, the operational semantics of the RETURN instruction is to return to the caller code block that invokes the current code block. Thus, during the Boogie code generation, we insert a fresh Boogie label after each code block invocation, denoted by END as shown in the translation rules of the INVOKE_CB and INVOKE_CB_S instructions (Table 5). Thus, our translation rule for the RETURN instruction simply goes to the END label and thus has the effect of returning the execution to the caller code block.

  4. 4.

    In Table 6, the OCLType#allInstance function used by the translation rule for the ALLINST instruction comes from our Boogie library for OCL [19]. It returns a sequence of the currently allocated elements on the given heap whose classifier is as specified by the input classifier name.

  5. 5.

    In Table 6, the default, referred by the translation rule for the REMOVE instruction, is a shorthand to represent the default value of EMF types in Boogie, e.g. the default value for boolean type is false, for integer type is 0, for string type is an empty sequence and for any other types is null.

  6. 6.

    In Table 6, the ExecEnv, referred by the translation rule for the GETENV and GETENVTYPE instructions, is a Boogie constant of type ref that represents the execution environment of EMFTVM. Currently, our formalisation for the EMFTVM bytecode language does not provide axioms to encode its semantics. This technical limitation requires more thorough examination for the source code of EMFTVM, which we are currently working on. This leads to the absence of the translation rule for EMFTVM instructions such as MATCH and MATCH_S, since these instructions require static information from the execution environment of EMFTVM.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Cheng, Z., Monahan, R. & Power, J.F. Formalised EMFTVM bytecode language for sound verification of model transformations. Softw Syst Model 17, 1197–1225 (2018). https://doi.org/10.1007/s10270-016-0553-x

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10270-016-0553-x

Keywords

Search

Navigation