{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:21:08Z","timestamp":1759033268814},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T00:00:00Z","timestamp":1330992000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1007\/s10515-012-0102-y","type":"journal-article","created":{"date-parts":[[2012,3,5]],"date-time":"2012-03-05T23:48:13Z","timestamp":1330991293000},"page":"5-46","source":"Crossref","is-referenced-by-count":49,"title":["Automated verification of model transformations based on visual contracts"],"prefix":"10.1007","volume":"20","author":[{"given":"Esther","family":"Guerra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"de Lara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerti","family":"Kappel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelika","family":"Kusel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Werner","family":"Retschitzegger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"Sch\u00f6nb\u00f6ck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wieland","family":"Schwinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,3,6]]},"reference":[{"key":"102_CR1","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-642-20116-5_11","volume-title":"Software and Data Technologies","author":"V. Aranega","year":"2011","unstructured":"Aranega, V., Mottu, J.-M., Etien, A., Dekeyser, J.-L.: Using trace to situate errors in model transformations. In: Software and Data Technologies. Communications in Computer and Information Science, vol. 50, pp. 137\u2013149. Springer, Berlin (2011)"},{"key":"102_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-642-17322-6_11","volume-title":"Graph Transformations and Model-Driven Engineering","author":"A. Balogh","year":"2010","unstructured":"Balogh, A., Bergmann, G., Csert\u00e1n, G., G\u00f6nczy, L., Horv\u00e1th, A., Majzik, I., Pataricza, A., Polg\u00e1r, B., R\u00e1th, I., Varr\u00f3, D., Varr\u00f3, G.: Workflow-driven tool integration using model transformations. In: Graph Transformations and Model-Driven Engineering. LNCS, vol. 5765, pp. 224\u2013248. Springer, Berlin (2010)"},{"key":"102_CR3","volume-title":"ECMDA Workshop on Integration of Model Driven Development and Model Driven Testing","author":"B. Baudry","year":"2006","unstructured":"Baudry, B., Dinh-Trong, T., Mottu, J., Simmonds, D., France, R., Ghosh, S., Fleurey, F., Le Traon, Y.: Model transformation testing challenges. In: ECMDA Workshop on Integration of Model Driven Development and Model Driven Testing, vol. 92 (2006)"},{"key":"102_CR4","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1145\/1743546.1743583","volume":"53","author":"B. Baudry","year":"2010","unstructured":"Baudry, B., Ghosh, S., Fleurey, F., France, R., Le Traon, Y., Mottu, J.-M.: Barriers to systematic model transformation testing. Commun. ACM 53, 139\u2013143 (2010)","journal-title":"Commun. ACM"},{"key":"102_CR5","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.774917","volume":"32","author":"A. Beugnard","year":"1999","unstructured":"Beugnard, A., J\u00e9z\u00e9quel, J.-M., Plouzeau, N., Watkins, D.: Making components contract aware. Computer 32, 38\u201345 (1999)","journal-title":"Computer"},{"issue":"2","key":"102_CR6","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10270-005-0079-0","volume":"4","author":"J. B\u00e9zivin","year":"2005","unstructured":"B\u00e9zivin, J.: On the unification power of models. Softw. Syst. Model. 4(2), 31 (2005)","journal-title":"Softw. Syst. Model."},{"key":"102_CR7","volume-title":"Workshop of MoDELS\u201905","author":"J. B\u00e9zivin","year":"2005","unstructured":"B\u00e9zivin, J., Rumpe, B., Sch\u00fcrr, A., Tratt, L.: Model transformations in practice. In: Workshop of MoDELS\u201905 (2005)"},{"issue":"7","key":"102_CR8","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1002\/spe.520","volume":"33","author":"L.C. Briand","year":"2003","unstructured":"Briand, L.C., Labiche, Y., Sun, H.: Investigating the use of analysis contracts to improve the testability of object-oriented code. Softw. Pract. Exp. 33(7), 637\u2013672 (2003)","journal-title":"Softw. Pract. Exp."},{"key":"102_CR9","first-page":"85","volume-title":"ISSRE\u201906","author":"E. Brottier","year":"2006","unstructured":"Brottier, E., Fleurey, F., Steel, J., Baudry, B., Traon, Y.L.: Metamodel-based test generation for model transformations: an algorithm and a tool. In: ISSRE\u201906, pp. 85\u201394. IEEE Comput. Soc., Los Alamitos (2006)"},{"issue":"2","key":"102_CR10","doi-asserted-by":"crossref","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. J. Syst. Softw. 83(2), 283\u2013302 (2010)","journal-title":"J. Syst. Softw."},{"key":"102_CR11","first-page":"69","volume-title":"Workshop on OCL and Model Driven Engineering UML\u201904","author":"E. Cariou","year":"2004","unstructured":"Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: Workshop on OCL and Model Driven Engineering UML\u201904, vol. 12, pp. 69\u201383 (2004)"},{"key":"102_CR12","series-title":"24","volume-title":"ECEASST","author":"E. Cariou","year":"2009","unstructured":"Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations. In: ECEASST, vol.\u00a024 (2009)"},{"issue":"3","key":"102_CR13","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1147\/sj.453.0621","volume":"45","author":"K. Czarnecki","year":"2006","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J. 45(3), 621\u2013645 (2006)","journal-title":"IBM Syst. J."},{"key":"102_CR14","unstructured":"EMF: Eclipse Modeling Framework. www.eclipse.org\/emf . Last accessed: January 2012"},{"key":"102_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3552-9","volume-title":"Discrete-Event Simulation: Modeling, Programming, and Analysis","author":"G.S. Fishman","year":"2001","unstructured":"Fishman, G.S.: Discrete-Event Simulation: Modeling, Programming, and Analysis. Springer, Berlin (2001)"},{"key":"102_CR16","first-page":"29","volume-title":"MoDeVa\u201904","author":"F. Fleurey","year":"2004","unstructured":"Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: testing model transformations. In: MoDeVa\u201904, pp. 29\u201340. IEEE Comput. Soc., Los Alamitos (2004)"},{"key":"102_CR17","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10270-007-0074-8","volume":"8","author":"F. Fleurey","year":"2009","unstructured":"Fleurey, F., Baudry, B., Muller, P.-A., Traon, Y.: Qualifying input test data for model transformations. Softw. Syst. Model. 8, 185\u2013203 (2009)","journal-title":"Softw. Syst. Model."},{"key":"102_CR18","first-page":"37","volume-title":"FOSE\u201907","author":"R. France","year":"2007","unstructured":"France, R., Rumpe, B.: Model-driven development of complex software: A research roadmap. In: FOSE\u201907, pp. 37\u201354. IEEE Comput. Soc., Los Alamitos (2007)"},{"key":"102_CR19","series-title":"LNCS","first-page":"748","volume-title":"MODELS\u201909","author":"P. Giner","year":"2009","unstructured":"Giner, P., Pelechano, V.: Test-driven development of model transformations. In: MODELS\u201909. LNCS, vol. 5795, pp. 748\u2013752. Springer, Berlin (2009)"},{"key":"102_CR20","series-title":"LNCS","first-page":"221","volume-title":"ECMFA\u201911","author":"M. Gogolla","year":"2011","unstructured":"Gogolla, M., Vallecillo, A.: Tractable model transformation testing. In: ECMFA\u201911. LNCS, vol. 6698, pp. 221\u2013235. Springer, Berlin (2011)"},{"key":"102_CR21","volume-title":"Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit","author":"R.C. Gronback","year":"2009","unstructured":"Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley Professional, Reading (2009). See also http:\/\/www.eclipse.org\/modeling\/gmp\/"},{"key":"102_CR22","first-page":"119","volume-title":"VL\/HCC","author":"E. Guerra","year":"2010","unstructured":"Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F.: A visual specification language for model-to-model transformations. In: VL\/HCC, pp. 119\u2013126. IEEE Comput. Soc., Los Alamitos (2010)"},{"key":"102_CR23","doi-asserted-by":"crossref","unstructured":"Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F., dos Santos, O.M.: Engineering model transformations with transML. Softw. Syst. Mod. (2011, in press). doi: 10.1007\/s10270-011-0211-2","DOI":"10.1007\/s10270-011-0211-2"},{"key":"102_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":"102_CR25","series-title":"Monographs in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets Basic Concepts, Analysis Methods and Practical Use","author":"K. Jensen","year":"1997","unstructured":"Jensen, K.: Coloured Petri Nets Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science. Springer, Berlin (1997)"},{"issue":"3\u20134","key":"102_CR26","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K. Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3\u20134), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"102_CR27","volume-title":"Model Transformations in Practice Workshop","author":"F. Jouault","year":"2005","unstructured":"Jouault, F., Kurtev, I.: Transforming models with ATL. In: Model Transformations in Practice Workshop (2005)"},{"issue":"2","key":"102_CR28","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/s10515-010-0079-3","volume":"18","author":"M. Kessentini","year":"2011","unstructured":"Kessentini, M., Sahraoui, H.A., Boukadoum, M.: Example-based model-transformation testing. Autom. Softw. Eng. 18(2), 199\u2013224 (2011)","journal-title":"Autom. Softw. Eng."},{"key":"102_CR29","series-title":"LNCS","first-page":"46","volume-title":"ICMT\u201908","author":"D. Kolovos","year":"2008","unstructured":"Kolovos, D., Paige, R., Polack, F.: The Epsilon transformation language. In: ICMT\u201908. LNCS, vol. 5063, pp. 46\u201360. Springer, Berlin (2008a)"},{"key":"102_CR30","first-page":"97","volume-title":"ICSTW\u201908","author":"D. Kolovos","year":"2008","unstructured":"Kolovos, D., Paige, R., Rose, L., Polack, F.: Unit testing model management operations. In: ICSTW\u201908, pp. 97\u2013104. IEEE Comput. Soc., Los Alamitos (2008b)"},{"key":"102_CR31","first-page":"13","volume-title":"GaMMa\u201906","author":"D.S. Kolovos","year":"2006","unstructured":"Kolovos, D.S., Paige, R.F., Polack, F.A.: Model comparison: a foundation for model composition and model transformation testing. In: GaMMa\u201906, pp. 13\u201320. ACM Press, New York (2006)"},{"issue":"4","key":"102_CR32","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10270-006-0017-9","volume":"5","author":"T. K\u00fchne","year":"2006","unstructured":"K\u00fchne, T.: Matters of (meta-)modeling. Softw. Syst. Model. 5(4), 369\u2013385 (2006)","journal-title":"Softw. Syst. Model."},{"issue":"3","key":"102_CR33","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s10270-006-0018-8","volume":"5","author":"J.M. K\u00fcster","year":"2006","unstructured":"K\u00fcster, J.M.: Definition and validation of model transformations. Softw. Syst. Model. 5(3), 233\u2013259 (2006)","journal-title":"Softw. Syst. Model."},{"key":"102_CR34","series-title":"LNCS","first-page":"193","volume-title":"Models in Software Engineering","author":"J.M. K\u00fcster","year":"2006","unstructured":"K\u00fcster, J.M., Abd-El-Razik, M.: Validation of model transformations\u2014first experiences using a white box approach. In: Models in Software Engineering. LNCS, vol. 4364, pp. 193\u2013204. Springer, Berlin (2006)"},{"issue":"1\u20133","key":"102_CR35","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1\u20133), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"key":"102_CR36","volume-title":"OOPSLA Workshop on Best Practices for Model-Driven Software Development","author":"Y. Lin","year":"2004","unstructured":"Lin, Y., Zhang, J., Gray, J.: Model comparison: A key challenge for transformation testing and version control in model driven software development. In: OOPSLA Workshop on Best Practices for Model-Driven Software Development (2004)"},{"key":"102_CR37","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-28554-7_10","volume-title":"Model-Driven Software Development","author":"Y. Lin","year":"2005","unstructured":"Lin, Y., Zhang, J., Gray, J.: A testing framework for model transformations. In: Model-Driven Software Development, pp. 219\u2013236 (2005)"},{"key":"102_CR38","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.entcs.2005.10.021","volume":"152","author":"T. Mens","year":"2006","unstructured":"Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125\u2013142 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"102_CR39","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. Computer 25, 40\u201351 (1992)","journal-title":"Computer"},{"key":"102_CR40","series-title":"LNCS","first-page":"589","volume-title":"MoDELS\u201906","author":"J.-M. Mottu","year":"2006","unstructured":"Mottu, J.-M., Baudry, B., Le Traon, Y.: Reusable MDA components: A testing-for-trust approach. In: MoDELS\u201906. LNCS, vol. 4199, pp. 589\u2013603. Springer, Berlin (2006)"},{"key":"102_CR41","first-page":"105","volume-title":"ICSTW\u201908","author":"J.-M. Mottu","year":"2008","unstructured":"Mottu, J.-M., Baudry, B., Traon, Y.L.: Model transformation testing: oracle issue. In: ICSTW\u201908, pp. 105\u2013112. IEEE Comput. Soc., Los Alamitos (2008)"},{"key":"102_CR42","unstructured":"Object Management Group: OCL Specification Version 2.0. http:\/\/www.omg.org\/docs\/ptc\/05-06-06.pdf , 2005"},{"key":"102_CR43","unstructured":"Object Management Group: QVT Specification Version 1.1. http:\/\/www.omg.org\/spec\/QVT\/1.1\/ , 2011"},{"key":"102_CR44","series-title":"LNCS","first-page":"121","volume-title":"MoDELS\u201907","author":"R. Ramos","year":"2007","unstructured":"Ramos, R., Barais, O., J\u00e9z\u00e9quel, J.-M.: Matching model-snippets. In: MoDELS\u201907. LNCS, vol. 4735, pp. 121\u2013135. Springer, Berlin (2007)"},{"issue":"2","key":"102_CR45","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"D.C. Schmidt","year":"2006","unstructured":"Schmidt, D.C.: Model-driven engineering. Computer 39(2), 25\u201331 (2006)","journal-title":"Computer"},{"key":"102_CR46","series-title":"LNCS","first-page":"148","volume-title":"ICMT\u201909","author":"S. Sen","year":"2009","unstructured":"Sen, S., Baudry, B., Mottu, J.-M.: Automatic model generation strategies for model transformation testing. In: ICMT\u201909. LNCS, vol. 5563, pp. 148\u2013164. Springer, Berlin (2009)"},{"issue":"1","key":"102_CR47","doi-asserted-by":"crossref","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. 4(1), 40\u201350 (1989)","journal-title":"Softw. Eng. J."},{"key":"102_CR48","unstructured":"TATA Research Development and Design: ModelMorf. http:\/\/www.tcs-trddc.com\/trddc_website\/ModelMorf\/ModelMorf.htm . Last accessed: January 2012"},{"issue":"8","key":"102_CR49","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1109\/TSE.2006.79","volume":"32","author":"Y.L. Traon","year":"2006","unstructured":"Traon, Y.L., Baudry, B., J\u00e9z\u00e9quel, J.-M.: Design by contract to improve software vigilance. IEEE Trans. Softw. Eng. 32(8), 571\u2013586 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"102_CR50","series-title":"LNCS","first-page":"260","volume-title":"ICGT\u201906","author":"D. Varr\u00f3","year":"2006","unstructured":"Varr\u00f3, D., Varr\u00f3-Gyapay, S., Ehrig, H., Prange, U., Taentzer, G.: Termination analysis of model transformations by Petri nets. In: ICGT\u201906. LNCS, vol. 4178, pp. 260\u2013274. Springer, Berlin (2006)"},{"key":"102_CR51","unstructured":"Xpand: Xpand Templates. http:\/\/wiki.eclipse.org\/Xpand . Last accessed: January 2012"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0102-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-012-0102-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0102-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:16:11Z","timestamp":1559157371000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-012-0102-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,6]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["102"],"URL":"https:\/\/doi.org\/10.1007\/s10515-012-0102-y","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,6]]}}}