{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T19:03:41Z","timestamp":1769022221530,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642388828","type":"print"},{"value":"9783642388835","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38883-5_15","type":"book-chapter","created":{"date-parts":[[2013,6,12]],"date-time":"2013-06-12T01:26:40Z","timestamp":1371000400000},"page":"158-173","source":"Crossref","is-referenced-by-count":7,"title":["Checking Model Transformation Refinement"],"prefix":"10.1007","author":[{"given":"Fabian","family":"B\u00fcttner","sequence":"first","affiliation":[]},{"given":"Marina","family":"Egea","sequence":"additional","affiliation":[]},{"given":"Esther","family":"Guerra","sequence":"additional","affiliation":[]},{"given":"Juan","family":"de Lara","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K. Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Software and Systems Modeling\u00a09(1), 69\u201386 (2010)","journal-title":"Software and Systems Modeling"},{"key":"15_CR2","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster, J.M.: Analysis of model transformations via alloy. In: MODEVVA 2007 (2007)"},{"key":"15_CR3","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1998)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/11880240_31","volume-title":"Model Driven Engineering Languages and Systems","author":"J. B\u00e9zivin","year":"2006","unstructured":"B\u00e9zivin, J., B\u00fcttner, F., Gogolla, M., Jouault, F., Kurtev, I., Lindow, A.: Model transformations? Transformation models! In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol.\u00a04199, pp. 440\u2013453. Springer, Heidelberg (2006)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-642-33666-9_28","volume-title":"Model Driven Engineering Languages and Systems","author":"F. B\u00fcttner","year":"2012","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol.\u00a07590, pp. 432\u2013448. Springer, Heidelberg (2012)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-34281-3_16","volume-title":"Formal Methods and Software Engineering","author":"F. B\u00fcttner","year":"2012","unstructured":"B\u00fcttner, 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.\u00a07635, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"issue":"2","key":"15_CR7","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., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software\u00a083(2), 283\u2013302 (2010)","journal-title":"Journal of Systems and Software"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML\/OCL models using constraint programming. In: ASE 2007, ACM (2007)","DOI":"10.1145\/1321631.1321737"},{"key":"15_CR9","unstructured":"Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: OCL Workshop, vol.\u00a012, pp. 69\u201383 (2004)"},{"key":"15_CR10","first-page":"1","volume":"24","author":"M. Clavel","year":"2009","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking Unsatisfiability for OCL Constraints. Electronic Communications of the EASST\u00a024, 1\u201313 (2009)","journal-title":"Electronic Communications of the EASST"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-30476-7_3","volume-title":"Theory and Practice of Model Transformations","author":"E. Guerra","year":"2012","unstructured":"Guerra, E.: Specification-driven test generation for model transformations. In: Hu, Z., de Lara, J. (eds.) ICMT 2012. LNCS, vol.\u00a07307, pp. 40\u201355. Springer, Heidelberg (2012)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Guerra, E., de Lara, J., Kolovos, D., Paige, R., dos Santos, O.: Engineering model transformations with transML. Software and Systems Modeling (2012) (in press)","DOI":"10.1007\/s10270-011-0211-2"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F.: A visual specification language for model-to-model transformations. In: VL\/HCC 2010, pp. 119\u2013126. IEEE CS (2010)","DOI":"10.1109\/VLHCC.2010.25"},{"issue":"1","key":"15_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-012-0102-y","volume":"20","author":"E. Guerra","year":"2013","unstructured":"Guerra, E., de Lara, J., Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Sch\u00f6nb\u00f6ck, J., Schwinger, W.: Automated verification of model transformations based on visual contracts. Autom. Softw. Eng.\u00a020(1), 5\u201346 (2013)","journal-title":"Autom. Softw. Eng."},{"key":"15_CR15","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT (2012)"},{"issue":"1-2","key":"15_CR16","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.08.002","volume":"72","author":"F. Jouault","year":"2008","unstructured":"Jouault, F., Allilaire, F., B\u00e9zivin, J., Kurtev, I.: ATL: A model transformation tool. Sci. Comp. Pr.\u00a072(1-2), 31\u201339 (2008)","journal-title":"Sci. Comp. Pr."},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-21952-8_21","volume-title":"Objects, Models, Components, Patterns","author":"M. Kuhlmann","year":"2011","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol.\u00a06705, pp. 290\u2013306. Springer, Heidelberg (2011)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"OMG OCL Specification, version 2.3.1 (Document formal\/2012-01-01) (2012)","DOI":"10.5530\/pc.2012.3.1"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-04164-8_8","volume-title":"Semantics and Algebraic Specification","author":"F. Orejas","year":"2009","unstructured":"Orejas, F., Wirsing, M.: On the specification and verification of model transformations. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol.\u00a05700, pp. 140\u2013161. Springer, Heidelberg (2009)"},{"issue":"2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/2089116.2089123","volume":"21","author":"A. Queralt","year":"2012","unstructured":"Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. TOSEM\u00a021(2), 13 (2012)","journal-title":"TOSEM"},{"key":"15_CR21","unstructured":"QVT (2005), http:\/\/www.omg.org\/spec\/QVT\/1.0\/PDF\/ (last accessed November 2010)"},{"key":"15_CR22","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)"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1049\/sej.1989.0006","volume":"4","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: An introduction to Z and formal specifications. Softw. Eng. J.\u00a04(1), 40\u201350 (1989)","journal-title":"Softw. Eng. J."},{"issue":"4","key":"15_CR24","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10270-006-0036-6","volume":"6","author":"J. Steel","year":"2007","unstructured":"Steel, J., J\u00e9z\u00e9quel, J.-M.: On model typing. SoSyM\u00a06(4), 401\u2013413 (2007)","journal-title":"SoSyM"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-30476-7_4","volume-title":"Theory and Practice of Model Transformations","author":"A. Vallecillo","year":"2012","unstructured":"Vallecillo, A., Gogolla, M.: Typing model transformations using Tracts. In: Hu, Z., de Lara, J. (eds.) ICMT 2012. LNCS, vol.\u00a07307, pp. 56\u201371. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Model Transformations"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38883-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,28]],"date-time":"2020-07-28T06:52:40Z","timestamp":1595919160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38883-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388828","9783642388835"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38883-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}