{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T15:14:55Z","timestamp":1773501295707,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544938","type":"print"},{"value":"9783662544945","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54494-5_17","type":"book-chapter","created":{"date-parts":[[2017,3,22]],"date-time":"2017-03-22T00:09:02Z","timestamp":1490141342000},"page":"300-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A Deductive Approach for Fault Localization in ATL Model Transformations"],"prefix":"10.1007","author":[{"given":"Zheng","family":"Cheng","sequence":"first","affiliation":[]},{"given":"Massimo","family":"Tisi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,22]]},"reference":[{"key":"17_CR1","unstructured":"A deductive approach for fault localization in ATL model transformations (2016). https:\/\/goo.gl\/xssbpn"},{"key":"17_CR2","unstructured":"Ab. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015)"},{"issue":"6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Aranega, V., Mottu, J., Etien, A., Dekeyser, J.: Traceability mechanism for error localization in model transformation. In: 4th International Conference on Software and Data Technologies, Sofia, Bulgaria, pp. 66\u201373 (2009)","DOI":"10.5220\/0002264700660073"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi:10.1007\/11804192_17"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-79707-4_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"G Berry","year":"2008","unstructured":"Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and esterel. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 2\u20132. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-79707-4_2"},{"key":"17_CR7","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)","edition":"1"},{"issue":"5","key":"17_CR8","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1109\/TSE.2014.2375201","volume":"41","author":"L Burgue\u00f1o","year":"2015","unstructured":"Burgue\u00f1o, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Softw. Eng. 41(5), 490\u2013506 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_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. 7590, pp. 432\u2013448. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33666-9_28"},{"key":"17_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. 7635, pp. 198\u2013213. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-34281-3_16"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19829-8_8","volume-title":"Formal Methods: Foundations and Applications","author":"D Calegari","year":"2011","unstructured":"Calegari, D., Luna, C., Szasz, N., Tasistro, \u00c1.: A type-theoretic framework for certified model transformations. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 112\u2013127. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19829-8_8"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-21155-8_11","volume-title":"Theory and Practice of Model Transformations","author":"Z Cheng","year":"2015","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: Kolovos, D., Wimmer, M. (eds.) ICMT 2015. LNCS, vol. 9152, pp. 133\u2013148. Springer, Cham (2015). doi:10.1007\/978-3-319-21155-8_11"},{"issue":"9","key":"17_CR13","doi-asserted-by":"publisher","first-page":"943","DOI":"10.4304\/jsw.4.9.943-958","volume":"4","author":"B Combemale","year":"2009","unstructured":"Combemale, B., Cr\u00e9gut, X., Garoche, P., Thirioux, X.: Essay on semantics definition in MDE - an instrumented approach for model verification. J. Softw. 4(9), 943\u2013958 (2009)","journal-title":"J. Softw."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: 25th IEEE International Symposium on Software Reliability Engineering, pp. 34\u201344. IEEE, Naples (2014)","DOI":"10.1109\/ISSRE.2014.10"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-37036-6_8"},{"key":"17_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science Modelling and Reasoning About Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)"},{"issue":"5","key":"17_CR17","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1\u20132","key":"17_CR18","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. 72(1\u20132), 31\u201339 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"17_CR19","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00165-014-0313-z","volume":"27","author":"K Lano","year":"2014","unstructured":"Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193\u2013235 (2014)","journal-title":"Formal Aspects Comput."},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Oakes, B.J., Troya, J., L\u00facio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: 18th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 256\u2013265. IEEE, Ottawa (2015)","DOI":"10.1109\/MODELS.2015.7338256"},{"key":"17_CR22","unstructured":"Object Management Group: The Object Constraint Language Specification (ver. 2.0) (2006). http:\/\/www.omg.org\/spec\/OCL\/2.0\/"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-16901-4_6","volume-title":"Formal Methods and Software Engineering","author":"I Poernomo","year":"2010","unstructured":"Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in Coq. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 56\u201373. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-16901-4_6"},{"issue":"7","key":"17_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/2856103","volume":"59","author":"A Roychoudhury","year":"2016","unstructured":"Roychoudhury, A., Chandra, S.: Formula-based software debugging. Commun. ACM 59(7), 68\u201377 (2016)","journal-title":"Commun. ACM"},{"key":"17_CR25","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":"GMK 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. 7349, pp. 90\u2013101. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31491-9_9"},{"key":"17_CR26","volume-title":"EMF: Eclipse Modeling Framework","author":"D Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework, 2nd edn. Pearson Education, London (2008)","edition":"2"},{"key":"17_CR27","unstructured":"Tip, F.: A survey of program slicing techniques. Technical report, Centrum Wiskunde & Informatica (1994)"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1007\/978-3-642-41533-3_40","volume-title":"Model-Driven Engineering Languages and Systems","author":"M Tisi","year":"2013","unstructured":"Tisi, M., Mart\u00ednez, S., Choura, H.: Parallel execution of ATL transformation rules. In: Moreira, A., Sch\u00e4tz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 656\u2013672. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-41533-3_40"},{"key":"17_CR29","unstructured":"Wagelaar, D.: Using ATL\/EMFTVM for import\/export of medical data. In: 2nd Software Development Automation Conference, Amsterdam, Netherlands (2014)"},{"key":"17_CR30","unstructured":"Weiser, M.: Program slicing. In: 5th International Conference on Software Engineering, pp. 439\u2013449. IEEE, New Jersey (1981)"},{"key":"17_CR31","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. Pre-Print (99), 1\u201341 (2016)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54494-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:18:57Z","timestamp":1750173537000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54494-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544938","9783662544945"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54494-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"22 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}