Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 4/2018

16.08.2016 | Regular Paper

Formalised EMFTVM bytecode language for sound verification of model transformations

verfasst von: Zheng Cheng, Rosemary Monahan, James F. Power

Erschienen in: Software and Systems Modeling | Ausgabe 4/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel A model-driven development approach for context-aware systems
Nächster Artikel Scope in model transformations

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Notice that when the ATL transformation is compiled into an EMFTVM implementation, the second binding always overwrites the first binding (Sect. 6.3).
 
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.
 
Literatur
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)CrossRef
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)CrossRef
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)
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)CrossRef
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)CrossRef
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.
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)CrossRef
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)CrossRef
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)CrossRef
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.
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)MathSciNetCrossRefMATH
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)CrossRef
34.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefMATH
35.
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)CrossRefMATH
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)CrossRef
38.
39.
Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1–2), 31–39 (2008)MathSciNetCrossRefMATH
40.
41.
Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman, Boston (2003)
42.
Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193–235 (2014)MathSciNetCrossRefMATH
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.
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
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)CrossRef
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)CrossRef
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)
60.
Syriani, E., Vangheluwe, H.: A modular timed graph transformation language for simulation-based design. Softw. Syst. Model. 12(2), 387–414 (2013)CrossRef
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)
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.
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)
Metadaten
Titel
Formalised EMFTVM bytecode language for sound verification of model transformations
verfasst von
Zheng Cheng
Rosemary Monahan
James F. Power
Publikationsdatum
16.08.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2018
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-016-0553-x

Weitere Artikel der Ausgabe 4/2018

Software and Systems Modeling 4/2018 Zur Ausgabe

Regular Paper

The Train Benchmark: cross-technology performance evaluation of continuous model queries

Regular Paper

A model-driven development approach for context-aware systems

Editorial

Agile model-based system development

Regular Paper

Encoding process discovery problems in SMT

Regular Paper

Efficient parallel reasoning on fuzzy goal models for run time requirements verification

Regular Paper

Reusing metamodels and notation with Diagram Definition

Premium Partner

    Bildnachweise