{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:53:51Z","timestamp":1761929631399},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642336539"},{"type":"electronic","value":"9783642336546"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33654-6_17","type":"book-chapter","created":{"date-parts":[[2012,9,18]],"date-time":"2012-09-18T03:47:41Z","timestamp":1347940061000},"page":"249-263","source":"Crossref","is-referenced-by-count":8,"title":["Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking"],"prefix":"10.1007","author":[{"given":"Holger","family":"Giese","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leen","family":"Lambers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1995","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall International (UK) Ltd., Hertfordshire (1995)"},{"key":"17_CR2","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 2003 Workshop. Number TUM-I0323 in Technical Report, Technische Universitat Munchen, pp. 63\u201378 (September 2003)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-69100-6_7","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"G. Engels","year":"2008","unstructured":"Engels, G., Kleppe, A., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: From UML Activities to TAAL - Towards Behaviour-Preserving Model Transformations. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol.\u00a05095, pp. 94\u2013109. Springer, Heidelberg (2008)"},{"key":"17_CR4","unstructured":"Narayanan, A., Karsai, G.: Verifying Model Transformations by Structural Correspondence. Electronic Communications of the EASST: Graph Transformation and Visual Modeling Techniques 2008 10 (2008)"},{"key":"17_CR5","unstructured":"Giese, H., Glesner, S., Leitner, J., Sch\u00e4fer, W., Wagner, R.: Towards Verified Model Transformations. In: Hearnden, D., S\u00fc\u00df, J., Baudry, B., Rapin, N. (eds.) Proc. of the 3rd International Workshop on Model Development, Validation and Verification (MoDeV2a). Genova, Italy, Le Commissariat \u00e0 l\u2019Energie Atomique - CEA, pp. 78\u201393 (October 2006)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16265-7_14","volume-title":"Integrated Formal Methods","author":"M. H\u00fclsbusch","year":"2010","unstructured":"H\u00fclsbusch, M., K\u00f6nig, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 183\u2013198. Springer, Heidelberg (2010)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-540-87405-8_17","volume-title":"Graph Transformations","author":"G. Rangel","year":"2008","unstructured":"Rangel, G., Lambers, L., K\u00f6nig, B., Ehrig, H., Baldan, P.: Behavior Preservation in Model Refactoring using DPO Transformations with Borrowed Contexts. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol.\u00a05214, pp. 242\u2013256. Springer, Heidelberg (2008)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-642-10248-6_13","volume-title":"Architecting Dependable Systems VI","author":"D. Bisztray","year":"2009","unstructured":"Bisztray, D., Heckel, R., Ehrig, H.: Compositional Verification of Architectural Refactorings. In: de Lemos, R., Fabre, J.-C., Gacek, C., Gadducci, F., ter Beek, M. (eds.) Architecting Dependable Systems VI. LNCS, vol.\u00a05835, pp. 308\u2013333. Springer, Heidelberg (2009)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-59071-4_45","volume-title":"Graph-Theoretic Concepts in Computer Science","author":"A. Sch\u00fcrr","year":"1995","unstructured":"Sch\u00fcrr, A.: Specification of Graph Translators with Triple Graph Grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol.\u00a0903, pp. 151\u2013163. Springer, Heidelberg (1995)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In: Proc. of the 28th International Conference on Software Engineering (ICSE), Shanghai, China. ACM Press (2006)","DOI":"10.1145\/1134285.1134297"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-21732-6_9","volume-title":"Theory and Practice of Model Transformations","author":"B. Becker","year":"2011","unstructured":"Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative Development of Consistency-Preserving Rule-Based Refactorings. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol.\u00a06707, pp. 123\u2013137. Springer, Heidelberg (2011)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Giese, H., Hildebrandt, S., Lambers, L.: Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars - Ensuring Conformance of Relational Model Transformation Specifications and Implementations. Software and Systems Modeling (2012)","DOI":"10.1007\/s10270-012-0247-y"},{"key":"17_CR13","series-title":"LNCS","first-page":"141","volume-title":"ICGT 2012","author":"U. Golas","year":"2012","unstructured":"Golas, U., Lambers, L., Ehrig, H., Giese, H.: Toward Bridging the Gap between Formal Foundations and Current Practice for Triple Graph Grammars. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol.\u00a07562, pp. 141\u2013155. Springer, Heidelberg (2012)"},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0960129508007202","volume":"19","author":"A. Habel","year":"2009","unstructured":"Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science\u00a019, 1\u201352 (2009)","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: M-adhesive transformation systems with nested application conditions, part 1: Parallelism, concurrency and amalgamation. Mathematical Structures in Computer Science (to appear, 2012)","DOI":"10.3233\/FI-2012-705"},{"issue":"3\/4","key":"17_CR16","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","volume":"26","author":"A. Habel","year":"1996","unstructured":"Habel, A., Heckel, R., Taentzer, G.: Graph Grammars with Negative Application Conditions. Fundamenta Informaticae\u00a026(3\/4), 287\u2013313 (1996)","journal-title":"Fundamenta Informaticae"},{"key":"17_CR17","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-19811-3_12","volume-title":"Fundamental Approaches to Software Engineering","author":"C. Ermel","year":"2011","unstructured":"Ermel, C., Gall, J., Lambers, L., Taentzer, G.: Modeling with Plausibility Checking: Inspecting Favorable and Critical Signs for Consistency between Control Flow and Functional Behavior. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 156\u2013170. Springer, Heidelberg (2011)"},{"key":"17_CR19","unstructured":"Pennemann, K.H.: Development of Correct Graph Transformation Systems. PhD thesis, Department of Computing Science, University of Oldenburg, Oldenburg (2009)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-45236-2_23","volume-title":"FME 2003: Formal Methods","author":"M. Charpentier","year":"2003","unstructured":"Charpentier, M.: Composing Invariants. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 401\u2013421. Springer, Heidelberg (2003)"},{"key":"17_CR21","unstructured":"Ehrig, H., Habel, A., Lambers, L.: Parallelism and Concurrency Theorems for Rules with Nested Application Conditions. In: Festschrift dedicated to Hans-Jorg Kreowski at the Occasion of his 60th Birthday. EC-EASST, vol.\u00a026 (2010)"},{"key":"17_CR22","unstructured":"Lambers, L.: Certifying Rule-Based Models using Graph Transformation. PhD thesis, Technische Universit\u00e4t Berlin (2010)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-78743-3_14","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Orejas","year":"2008","unstructured":"Orejas, F., Ehrig, H., Prange, U.: A Logic of Graph Constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 179\u2013198. Springer, Heidelberg (2008)"},{"key":"17_CR24","unstructured":"Blume, C., Bruggink, H.S., K\u00f6nig, B.: Recognizable Graph Languages for Checking Invariants. In: Proc. of GT-VMT 2010 (Workshop on Graph Transformation and Visual Modeling Techniques). Electronic Communications of the EASST, vol.\u00a029 (2010)"},{"issue":"2","key":"17_CR25","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/j.jss.2009.08.012","volume":"83","author":"J. Cabot","year":"2010","unstructured":"Cabot, J., Claris\u00f3, R., Guerra, E., Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw.\u00a083(2), 283\u2013302 (2010)","journal-title":"J. Syst. Softw."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: Upgrading Alloy with actions. In: Proc. of Int. Conf. of Software Engineering, pp. 442\u2013451. ACM (2005)","DOI":"10.1145\/1062455.1062535"}],"container-title":["Lecture Notes in Computer Science","Graph Transformations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33654-6_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,29]],"date-time":"2022-01-29T09:25:49Z","timestamp":1643448349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33654-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336539","9783642336546"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33654-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}