{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T00:08:46Z","timestamp":1715558926694},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,6,18]],"date-time":"2013-06-18T00:00:00Z","timestamp":1371513600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,5]]},"DOI":"10.1007\/s10270-013-0351-7","type":"journal-article","created":{"date-parts":[[2013,6,17]],"date-time":"2013-06-17T02:12:26Z","timestamp":1371435146000},"page":"981-1002","source":"Crossref","is-referenced-by-count":10,"title":["Formal verification of QVT transformations for code generation"],"prefix":"10.1007","volume":"14","author":[{"given":"Kurt","family":"Stenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Moebius","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,6,18]]},"reference":[{"key":"351_CR1","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: MODELS 2007\u201410TH International Conference on Model Driven Engineering Languages and Systems. Springer LNCS 4735 (2007)"},{"key":"351_CR2","doi-asserted-by":"crossref","unstructured":"Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: MODELS, Model Driven Engineering Languages and Systems, 13th International Conference. Springer LNCS 6394 (2010)","DOI":"10.1007\/978-3-642-16145-2_9"},{"key":"351_CR3","doi-asserted-by":"crossref","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Fundamental Approaches to Software Engineering. Springer LNCS 1783 (2000)","DOI":"10.1007\/3-540-46428-X_25"},{"key":"351_CR4","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software: The KeY Approach. Springer LNAI 4334 (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"351_CR5","doi-asserted-by":"crossref","unstructured":"Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: FASE 2009. Springer LNCS 5503 (2009)","DOI":"10.1007\/978-3-642-00593-0_2"},{"key":"351_CR6","unstructured":"Brucker, A., Krieger, M., Wolff, B.: Extending OCL with null-references: towards a formal semantics for OCL 2.1. In: MODELS 2009 Workshops. Springer LNCS 6002 (2010)"},{"key":"351_CR7","unstructured":"Brucker, A.D., Wolff, B.: The hol-ocl book. Technical Report 525, ETH Z\u00fcrich (2006)"},{"key":"351_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Kuhlmann, M.: Shortcomings of the embedding of OCL into QVT ImperativeOCL. In: Workshops and Symposia at MODELS\u201908. Springer LNCS 5421 (2009)","DOI":"10.1007\/978-3-642-01648-6_28"},{"key":"351_CR9","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2013.02.002","volume":"292","author":"D Calegari","year":"2013","unstructured":"Calegari, D., Szasz, N.: Verification of model transformations: a survey of the state-of-the-art. Electron. Notes Theor. Comput. Sci. 292, 5\u201325 (2013)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"351_CR10","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude: A High-Performance Logical Framework. Springer LNCS 4350 (2007)"},{"key":"351_CR11","doi-asserted-by":"crossref","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J. 45(3), 621\u2013645 (2006)","DOI":"10.1147\/sj.453.0621"},{"key":"351_CR12","doi-asserted-by":"crossref","unstructured":"Drossopoulou, S., Eisenbach, S.: Describing the semantics of Java and proving type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. Springer LNCS 1523 (1999)","DOI":"10.1007\/3-540-48737-9_2"},{"key":"351_CR13","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"H Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Heidelberg (2006)"},{"key":"351_CR14","doi-asserted-by":"crossref","unstructured":"Engels, G., Kleppe, A., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: From UML activities to TAAL: towards behaviour-preserving model transformations. In: ECMDA-FA 2008. Springer LNCS 5095 (2008)","DOI":"10.1007\/978-3-540-69100-6_7"},{"key":"351_CR15","doi-asserted-by":"crossref","unstructured":"Favre, L.: A formal foundation for metamodeling. In: Ada-Europe 2009, Proceedings. Springer LNCS 5570 (2009)","DOI":"10.1007\/978-3-642-01924-1_13"},{"key":"351_CR16","unstructured":"Giese, H., Glesner, S., Leitner, J., Sch\u00e4fer, W., Wagner, R.: Towards verified model transformations. In: Proceedings of the MoDeVa Workshop at MoDELS\u201906 (2006)"},{"key":"351_CR17","doi-asserted-by":"crossref","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69 (2007)","DOI":"10.1016\/j.scico.2007.01.013"},{"key":"351_CR18","doi-asserted-by":"crossref","unstructured":"Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL Models. In: Dubois, C. (ed.) Proceedings of 3rd International Conference Test and Proof (TAP\u20192009), pp. 90\u2013104. Springer, Berlin, LNCS 5668 (2009)","DOI":"10.1007\/978-3-642-02949-3_8"},{"key":"351_CR19","volume-title":"The Java (tm) Language Specification","author":"J Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java (tm) Language Specification, 3rd edn. Addison-Wesley, Boston (2005)","edition":"3"},{"key":"351_CR20","doi-asserted-by":"crossref","unstructured":"Grandy, H., Stenzel, K., Reif, W.: A refinement method for Java programs. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS). Springer LNCS 4468 (2007)","DOI":"10.1007\/978-3-540-72952-5_14"},{"key":"351_CR21","unstructured":"Haneberg, D., B\u00e4umler, S., Balser, M., Grandy, H., Ortmeier, F., Reif, W., Schellhorn, G., Schmitt, J., Stenzel, K.: The user interface of the KIV verification system: a system description. Electron. Notes Theor. Comput. Sci. UITP special issue (2006)"},{"key":"351_CR22","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"351_CR23","doi-asserted-by":"crossref","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fundamental Approaches to Software Engineering (FASE\u201900). Springer LNCS 1783 (2000)","DOI":"10.1007\/3-540-46428-X_20"},{"key":"351_CR24","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"351_CR25","doi-asserted-by":"crossref","unstructured":"Jouault, F., Kurtev, I.: On the architectural alignment of ATL and QVT. In: 21st ACM Symposium on Applied Computing. ACM Press, New York (2006)","DOI":"10.1145\/1141277.1141561"},{"issue":"1\u20132","key":"351_CR26","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.08.002","volume":"72","author":"Fr\u00e9d\u00e9ric Jouault","year":"2008","unstructured":"Jouault, Fr\u00e9d\u00e9ric, Allilaire, Freddy, B\u00e9zivin, Jean, Kurtev, Ivan, Valduriez, Patrick: ATL: a model transformation tool. Sci. Comput. Program. 72(1\u20132), 31\u201339 (2008)","journal-title":"Sci. Comput. Program."},{"key":"351_CR27","doi-asserted-by":"crossref","unstructured":"Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: Model Checking Software (SPIN). Springer LNCS 3925 (2006)","DOI":"10.1007\/11691617_19"},{"key":"351_CR28","unstructured":"KIV homepage. http:\/\/www.informatik.uni-augsburg.de\/swt\/kiv"},{"key":"351_CR29","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pp. 207\u2013220. ACM, Big Sky, MT, USA, October (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"351_CR30","unstructured":"Krieger, M., Knapp, A.: Executing underspecified OCL operation contracts with a SAT solver. In: Proceedings of the 8th International Workshop on OCL Concepts and Tools (OCL 2008) at MoDELS 2008. Electronic Communications of the EASST, vol. 15 (2008)"},{"issue":"2","key":"351_CR31","first-page":"233","volume":"6","author":"K Lano","year":"2012","unstructured":"Lano, K., Kolahdouz-Rahimi, S., Poernomo, I.: Comparative evaluation of model transformation specification approaches. Int. J. Softw. Inform. 6(2), 233\u2013269 (2012)","journal-title":"Int. J. Softw. Inform."},{"key":"351_CR32","unstructured":"Lucas, F.J., Toval, A.: Model transformations powered by rewriting logic. In: Proceedings of the Forum at the CAiSE\u201908 Conference. CEUR Workshop Proceedings, 2008. http:\/\/ftp.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-344\/"},{"key":"351_CR33","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Grandy, H., Reif, W.: SecureMDD: a model-driven development method for secure smart card applications. In: Workshop on Secure Software Engineering, SecSE, at ARES 2009. IEEE Press (2009)","DOI":"10.1109\/ARES.2009.22"},{"key":"351_CR34","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Modeling security-critical applications with UML in the secureMDD approach. Int. J. Adv. Softw. 1(1), 59\u201379 (2008)"},{"key":"351_CR35","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Generating formal specifications for security-critical applications: a model-driven approach. In: ICSE 2009 Workshop: International Workshop on Software Engineering for Secure Systems (SESS\u201909). IEEE\/ACM Digital Library (2009)","DOI":"10.1109\/IWSESS.2009.5068461"},{"key":"351_CR36","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Proceedings of ESSoS 2010: International Symposium on Engineering Secure Software and Systems. Springer LNCS 5965 (2010)","DOI":"10.1007\/978-3-642-11747-3_13"},{"key":"351_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, Berlin (2002)"},{"key":"351_CR38","unstructured":"Object Management Group (OMG). Meta Object Facility (MOF) 2.0 Query\/View\/Transformation Specification, Version 1.1 (2011)"},{"key":"351_CR39","unstructured":"Object Management Group (OMG). Meta Object Facility (MOF) Core, Version 2.4.1 (2011)"},{"key":"351_CR40","unstructured":"Object Management Group (OMG). Object Constraint Language, Version 2.3.1 (2012)"},{"key":"351_CR41","doi-asserted-by":"crossref","unstructured":"Queralt, A., Rull, G., Teniente, E., Farr\u00e9, C., Urp\u00ed, T.: AuRUS: automated reasoning on UML\/OCL schemas. In: ER 2010, 29th International Conference on Conceptual Modeling. Springer LNCS 6412 (2010)","DOI":"10.1007\/978-3-642-16373-9_32"},{"key":"351_CR42","unstructured":"QVT Operational (Eclipse Project). http:\/\/www.eclipse.org\/projects\/project_summary.php?projectid=modeling.m2m.qvt-oml"},{"key":"351_CR43","unstructured":"Rahim, L., Whittle, J.: Verifying semantic conformance of state machine-to-java code generators. In: MODELS 2010. Springer LNCS 6394 (2010)"},{"key":"351_CR44","doi-asserted-by":"crossref","unstructured":"Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Applications of Graph Transformations with Industrial Relevance (AGTIVE). Springer LNCS 3062 (2004)","DOI":"10.1007\/978-3-540-25959-6_40"},{"key":"351_CR45","unstructured":"Romeikat, R., Roser, S., M\u00fcllender, P., Bauer, B.: Translation of QVT relations into QVT operational mappings. In: ICMT 2008. Springer LNCS 5063 (2008)"},{"key":"351_CR46","doi-asserted-by":"crossref","unstructured":"Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, vol. 3. World Scientific Publishing Co., Singapore (1997)","DOI":"10.1142\/3303"},{"key":"351_CR47","unstructured":"The SAL symbolic analysis laboratory. http:\/\/sal.csl.sri.com\/"},{"key":"351_CR48","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 94: Graph-Theoretic Concepts in Computer Science. Springer LNCS 903 (1994)","DOI":"10.1007\/3-540-59071-4_45"},{"key":"351_CR49","unstructured":"SmartQVT. http:\/\/sourceforge.net\/projects\/smartqvt\/"},{"key":"351_CR50","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Dreschsler, R.: Encoding OCL data types for SAT-based verification of UML\/OCL models. In: Proceedings of the Conference on Tests and Proofs (TAP) 2011. Springer LNCS 6706 (2011)","DOI":"10.1007\/978-3-642-21768-5_12"},{"key":"351_CR51","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine: Definition, Verification, Validation","author":"RF St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Berlin (2001)"},{"key":"351_CR52","volume-title":"EMF Eclipse Modeling Framework","author":"D Steinberg","year":"2009","unstructured":"Steinberg, D., Budensky, F., Paternostro, M., Merks, E.: EMF Eclipse Modeling Framework, 2nd edn. Addison-Wesley, Boston (2009)","edition":"2"},{"key":"351_CR53","doi-asserted-by":"crossref","unstructured":"Stenzel, K.: A formally verified calculus for full Java Card. In: Algebraic Methodology and Software Technology (AMAST) 2004, Proceedings. Springer LNCS 3116 (2004)","DOI":"10.1007\/978-3-540-27815-3_37"},{"key":"351_CR54","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Faculty of Informatics, Augsburg University, Germany (2005)"},{"key":"351_CR55","doi-asserted-by":"crossref","unstructured":"Troya, J., Vallecillo, A.: Towards a rewriting logic semantics for ATL. In: ICMT 2010. Springer LNCS 6142 (2010)","DOI":"10.1007\/978-3-642-13688-7_16"},{"key":"351_CR56","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D\u00e1niel Varr\u00f3","year":"2004","unstructured":"Varr\u00f3, D\u00e1niel: Automated formal verification of visual modeling languages by model checking. Softw. Syst. Model. 3, 85\u2013113 (2004)","journal-title":"Softw. Syst. Model."},{"key":"351_CR57","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1016\/j.scico.2007.05.004","volume":"68","author":"D\u00e1niel Varr\u00f3","year":"2007","unstructured":"Varr\u00f3, D\u00e1niel, Balogh, Andr\u00e1s: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68, 214\u2013234 (2007)","journal-title":"Sci. Comput. Program."},{"key":"351_CR58","unstructured":"Varr\u00f3, D., Pataricza, A.: Automated formal verification of model transformations. In: J\u00fcrjens, J., Rumpe, B., France, R., Fernandez, E.B. (eds.) CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML\u201903 Workshop, number TUM-I0323 in Technical Report. Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"351_CR59","doi-asserted-by":"crossref","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the Java specification: proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. Springer LNCS 1523 (1999)","DOI":"10.1007\/3-540-48737-9_4"},{"key":"351_CR60","doi-asserted-by":"crossref","unstructured":"Wirsing, M.: Algebraic specification. In: Handbook of Theoretical Computer Science, vol B, chapter 13, pp. 675\u2013788. Elsevier, Oxford (1990)","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"351_CR61","unstructured":"XP and http:\/\/wiki.eclipse.org\/Xpand"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0351-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0351-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0351-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,12]],"date-time":"2024-05-12T13:02:04Z","timestamp":1715518924000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0351-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,18]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["351"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0351-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,18]]}}}