{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:50:44Z","timestamp":1725749444194},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642415326"},{"type":"electronic","value":"9783642415333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41533-3_42","type":"book-chapter","created":{"date-parts":[[2013,9,19]],"date-time":"2013-09-19T15:40:59Z","timestamp":1379605259000},"page":"690-706","source":"Crossref","is-referenced-by-count":6,"title":["Automated Verification of Model Transformations in the Automotive Industry"],"prefix":"10.1007","author":[{"given":"Gehan M. K.","family":"Selim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabian","family":"B\u00fcttner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James R.","family":"Cordy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juergen","family":"Dingel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shige","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","unstructured":"AUTOSAR Consortium. AUTOSAR System Template, \n                    \n                      http:\/\/AUTOSAR.org\/index.php?p=3&up=1&uup=3&uuup=3&uuuup=0&uuuuup=0\/AUTOSAR_TPS_SstemTemplate.pdf\n                    \n                    \n                   (2007)"},{"key":"42_CR2","unstructured":"AUTOSAR Consortium. AUTOSAR (2007), \n                    \n                      http:\/\/AUTOSAR.org\/"},{"key":"42_CR3","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster, J.: Analysis of Model Transformations via Alloy. MoDeVVa, pp. 47\u201356 (2007)"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Asztalos, M., Lengyel, L., Levendovszky, T.: Towards Automated, Formal Verification of Model Transformations. In: ICST, Paris, France, pp. 15\u201324 (2010)","DOI":"10.1109\/ICST.2010.42"},{"key":"42_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11841883_22","volume-title":"Graph Transformations","author":"L. Baresi","year":"2006","unstructured":"Baresi, L., Spoletini, P.: On the Use of Alloy to Analyze Graph Transformation Systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol.\u00a04178, pp. 306\u2013320. Springer, Heidelberg (2006)"},{"key":"42_CR6","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":"42_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-25032-3_8","volume-title":"Formal Methods, Foundations and Applications","author":"C. Braga","year":"2011","unstructured":"Braga, C., Menezes, R., Comicio, T., Santos, C., Landim, E.: On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol.\u00a07021, pp. 108\u2013123. Springer, Heidelberg (2011)"},{"issue":"4","key":"42_CR8","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s00236-009-0093-8","volume":"46","author":"A.D. Brucker","year":"2009","unstructured":"Brucker, A.D., Wolff, B.: Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica\u00a046(4), 255\u2013284 (2009)","journal-title":"Acta Informatica"},{"key":"42_CR9","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":"42_CR10","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":"42_CR11","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. Systems and Software\u00a083(2), 283\u2013302 (2010)","journal-title":"Systems and Software"},{"key":"42_CR12","unstructured":"Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL Contracts for the Verification of Model Transformations. EASST\u00a024 (2009)"},{"key":"42_CR13","unstructured":"Cottenier, T., Van Den Berg, A., Elrad, T.: The Motorola WEAVR: Model Weaving in a Large Industrial Context. In: AOSD, Vancouver, Canada, vol.\u00a032 (2007)"},{"key":"42_CR14","unstructured":"Daghsen, A., Chaaban, K., Saudrais, S., Leserf, P.: Applying Holistic Distributed Scheduling to AUTOSAR Methodology. In: ERTSS, Toulouse, France (2010)"},{"key":"42_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/978-3-642-17322-6_24","volume-title":"Graph Transformations and Model-Driven Engineering","author":"H. Giese","year":"2010","unstructured":"Giese, H., Hildebrandt, S., Neumann, S.: Model Synchronization at Work: Keeping sysML and AUTOSAR Models Consistent. In: Engels, G., Lewerentz, C., Sch\u00e4fer, W., Sch\u00fcrr, A., Westfechtel, B. (eds.) Nagl Festschrift. LNCS, vol.\u00a05765, pp. 555\u2013579. Springer, Heidelberg (2010)"},{"key":"42_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-21470-7_16","volume-title":"Modelling Foundations and Applications","author":"M. Gogolla","year":"2011","unstructured":"Gogolla, M., Vallecillo, A.: Tractable Model Transformation Testing. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol.\u00a06698, pp. 221\u2013235. Springer, Heidelberg (2011)"},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez P\u00e9rez, C.A., B\u00fcttner, F., Claris\u00f3, R., Cabot, J.: EMFtoCSP: A Tool for the Lightweight Verification of EMF Models. In: FormSERA, Zurich, Switzerland, pp. 44\u201350 (2012)","DOI":"10.1109\/FormSERA.2012.6229788"},{"issue":"1","key":"42_CR18","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. Automated Software Engineering\u00a020(1), 5\u201346 (2013)","journal-title":"Automated Software Engineering"},{"key":"42_CR19","doi-asserted-by":"crossref","unstructured":"Inaba, K., Hidaka, S., Hu, Z., Kato, H., Nakano, K.: Graph-Transformation Verification Using Monadic Second-Order Logic. In: PPDP, pp. 17\u201328 (2011)","DOI":"10.1145\/2003476.2003482"},{"key":"42_CR20","doi-asserted-by":"crossref","unstructured":"Jackson, E., Levendovszky, T., Balasubramanian, D.: Automatically reasoning about metamodeling. SoSyM, pp. 1\u201315 (2013)","DOI":"10.1007\/s10270-013-0315-y"},{"key":"42_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A Logic for the Java Modeling Language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"42_CR22","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. Comput. Program.\u00a072(1-2), 31\u201339 (2008)","journal-title":"Sci. Comput. Program."},{"key":"42_CR23","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":"42_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-16145-2_10","volume-title":"Model Driven Engineering Languages and Systems","author":"L. L\u00facio","year":"2010","unstructured":"L\u00facio, L., Barroca, B., Amaral, V.: A Technique for Automatic Validation of Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, \u00d8. (eds.) MODELS 2010, Part I. LNCS, vol.\u00a06394, pp. 136\u2013150. Springer, Heidelberg (2010)"},{"key":"42_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-540-69100-6_31","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"P. Mohagheghi","year":"2008","unstructured":"Mohagheghi, P., Dehlen, V.: Where is the Proof? - A Review of Experiences from Applying MDE in Industry. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol.\u00a05095, pp. 432\u2013443. Springer, Heidelberg (2008)"},{"key":"42_CR26","doi-asserted-by":"crossref","unstructured":"Narayanan, A., Karsai, G.: Verifying Model Transformations by Structural Correspondence. EASST\u00a010 (2008)","DOI":"10.1016\/j.entcs.2008.04.041"},{"issue":"2","key":"42_CR27","doi-asserted-by":"crossref","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":"42_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-68679-8_8","volume-title":"Concurrency, Graphs and Models","author":"A. Rensink","year":"2008","unstructured":"Rensink, A.: Explicit State Model Checking for Graph Grammars. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol.\u00a05065, pp. 114\u2013132. Springer, Heidelberg (2008)"},{"key":"42_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-31491-9_9","volume-title":"Modelling Foundations and Applications","author":"G.M.K. Selim","year":"2012","unstructured":"Selim, G.M.K., Wang, S., Cordy, J.R., Dingel, J.: Model Transformations for Migrating Legacy Models: An Industrial Case Study. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., St\u00f6rrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol.\u00a07349, pp. 90\u2013101. Springer, Heidelberg (2012)"},{"key":"42_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-04425-0_4","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Sen","year":"2009","unstructured":"Sen, S., Moha, N., Baudry, B., J\u00e9z\u00e9quel, J.-M.: Meta-model Pruning. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol.\u00a05795, pp. 32\u201346. Springer, Heidelberg (2009)"},{"key":"42_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-24485-8_39","volume-title":"Model Driven Engineering Languages and Systems","author":"K. Stenzel","year":"2011","unstructured":"Stenzel, K., Moebius, N., Reif, W.: Formal Verification of QVT Transformations for Code Generation. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol.\u00a06981, pp. 533\u2013547. Springer, Heidelberg (2011)"},{"key":"42_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-02674-4_3","volume-title":"Model Driven Architecture - Foundations and Applications","author":"M. Tisi","year":"2009","unstructured":"Tisi, M., Jouault, F., Fraternali, P., Ceri, S., B\u00e9zivin, J.: On the Use of Higher-Order Model Transformations. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol.\u00a05562, pp. 18\u201333. Springer, Heidelberg (2009)"},{"key":"42_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"issue":"5","key":"42_CR34","first-page":"1","volume":"10","author":"J. Troya","year":"2011","unstructured":"Troya, J., Vallecillo, A.: A Rewriting Logic Semantics for ATL. Journal of Object Technology\u00a010(5), 1\u201329 (2011)","journal-title":"Journal of Object Technology"},{"key":"42_CR35","unstructured":"The USE Validator, \n                    \n                      http:\/\/sourceforge.net\/projects\/useocl\/files\/Plugins\/ModelValidator\/"},{"key":"42_CR36","unstructured":"The ATL Transformation Zoo, \n                    \n                      http:\/\/www.eclipse.org\/atl\/atlTransformations\/\n                    \n                    \n                  ."}],"container-title":["Lecture Notes in Computer Science","Model-Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41533-3_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T12:02:55Z","timestamp":1558094575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41533-3_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415326","9783642415333"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41533-3_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}