{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T19:42:18Z","timestamp":1774640538247,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T00:00:00Z","timestamp":1416528000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10009-014-0356-8","type":"journal-article","created":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T11:02:05Z","timestamp":1416567725000},"page":"265-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Complete model-based equivalence class testing"],"prefix":"10.1007","volume":"18","author":[{"given":"Wen-ling","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,11,21]]},"reference":[{"issue":"8","key":"356_CR1","doi-asserted-by":"crossref","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","volume":"86","author":"Saswat Anand","year":"2013","unstructured":"Anand, Saswat, Burke, Edmund K., Chen, Tsong Yueh, Clark, John A., Cohen, Myra B., Grieskamp, W., Harman, M., Harrold, M.J., McMinn, P.: An orchestrated survey of methodologies for automated software test case generation. J. Syst. Softw. 86(8), 1978\u20132001 (2013)","journal-title":"J. Syst. Softw."},{"key":"356_CR2","volume-title":"Testing object-oriented systems: models, patterns, and tools","author":"RV Binder","year":"2000","unstructured":"Binder, R.V.: Testing object-oriented systems: models, patterns, and tools. Addison-Wesley, Reading (2000)"},{"issue":"5","key":"356_CR3","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1007\/s00165-012-0222-y","volume":"25","author":"AD Brucker","year":"2013","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Asp. Comput. 25(5), 683\u2013721 (2013)","journal-title":"Formal Asp. Comput."},{"key":"356_CR4","doi-asserted-by":"crossref","unstructured":"Chen, T.Y., Tse, T.H., Yu, Y.T.: Proportional sampling strategy: a compendium and some insights. J. Syst. Softw. 58(1), 65\u201381 (2001)","DOI":"10.1016\/S0164-1212(01)00028-0"},{"key":"356_CR5","doi-asserted-by":"crossref","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 4(3), 178\u2013187 (1978)","DOI":"10.1109\/TSE.1978.231496"},{"key":"356_CR6","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"356_CR7","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME \u201993: Industrial-strength formal methods. Lecture notes in computer science","author":"Jeremy Dick","year":"1993","unstructured":"Dick, Jeremy, Faivre, Alain: Automating the generation and sequencing of test cases from model-based specifications. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME \u201993: Industrial-strength formal methods. Lecture notes in computer science, pp. 268\u2013284. Springer, Berlin (1993)"},{"issue":"2","key":"356_CR8","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/j.entcs.2005.05.038","volume":"146","author":"F Doucet","year":"2006","unstructured":"Doucet, F., Menarini, M., Kr\u00fcger, I.H., Gupta, R.K., Talpin, J.-P.: A verification approach for gals integration of synchronous components. Electr. Notes Theor. Comput. Sci. 146(2), 105\u2013131 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"356_CR9","unstructured":"European Committee for Electrotechnical Standardization: EN 50128\u2014Railway applications\u2014Communications, signalling and processing systems\u2014Software for railway control and protection systems. CENELEC, Brussels (2001)"},{"key":"356_CR10","unstructured":"European Railway Agency: ERTMS\u2014System Requirements Specification\u2014UNISIG SUBSET-026 February 2012. http:\/\/www.era.europa.eu\/Document-Register\/Pages\/Set-2-System-Requirements-Specification.aspx"},{"key":"356_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-31848-4_1","volume-title":"Formal approaches to software testing. Lecture notes in computer science","author":"L Frantzen","year":"2005","unstructured":"Frantzen, L., Tretmans, J., Willemse, Tim A.C.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) Formal approaches to software testing. Lecture notes in computer science, pp. 1\u201315. Springer, Berlin (2005)"},{"issue":"6","key":"356_CR12","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1109\/32.87284","volume":"17","author":"S Fujiwara","year":"1991","unstructured":"Fujiwara, S., Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models. IEEE Trans. Softw. Eng. 17(6), 591\u2013603 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"356_CR13","first-page":"82","volume-title":"TAPSOFT. Lecture Notes in Computer Science","author":"M-C Gaudel","year":"1995","unstructured":"Gaudel, M.-C.: Testing can be formal, too. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) TAPSOFT. Lecture Notes in Computer Science, pp. 82\u201396. Springer, Berlin (1995)"},{"key":"356_CR14","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Latella, D., Massink, M.: Formal test-case generation for uml statecharts. In: Ninth IEEE International Conference on Engineering Complex Computer Systems (ICECCS\u201904), iceccs, pp. 75\u201384 (2004)","DOI":"10.1109\/ICECCS.2004.1310906"},{"key":"356_CR15","unstructured":"Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)"},{"issue":"4","key":"356_CR16","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1145\/566171.566190","volume":"27","author":"W Grieskamp","year":"2002","unstructured":"Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. ACM SIGSOFT Softw. Eng. Notes 27(4), 112\u2013122 (2002)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"356_CR17","doi-asserted-by":"crossref","unstructured":"Helke, S., Neustupny, T., Santen, T.: Automating test case generation from z specifications with isabelle. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM \u201997: The Z Formal Specification Notation, vol. 1212. Lecture Notes in Computer Science, pp. 52\u201371. Springer, Berlin (1997)","DOI":"10.1007\/BFb0027283"},{"key":"356_CR18","first-page":"327","volume-title":"TACAS. Lecture Notes in Computer Science","author":"HS Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS. Lecture Notes in Computer Science, pp. 327\u2013341. Springer, Berlin (2002)"},{"key":"356_CR19","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-642-41707-8_4","volume-title":"Testing software and systems. Lecture notes in computer science","author":"Wen-ling Huang","year":"2013","unstructured":"Huang, Wen-ling, Peleska, Jan: Exhaustive model-based equivalence class testing. In: Yenig\u00fcn, H\u00fcsn\u00fc, Yilmaz, Cemal, Ulrich, Andreas (eds.) Testing software and systems. Lecture notes in computer science, pp. 49\u201364. Springer, Berlin (2013)"},{"key":"356_CR20","unstructured":"Huang, W., Peleska, J., Schulze, U.: Comprehensive modelling for advanced systems of systems\u2014test automation support. Public Document D34.1, COMPASS, October 2013. http:\/\/www.compass-research.eu\/deliverables.html"},{"key":"356_CR21","unstructured":"ISO\/DIS 26262-4 Road vehicles\u2014Functional safety\u2014Part 4: Product development: system level. Technical report, International Organization for Standardization (2009)"},{"key":"356_CR22","unstructured":"ISO\/IEC\/IEEE 29119-1:2013(e): Software and systems engineering\u2014software testing\u2014part 1: Concepts and definitions, Sept (2013)"},{"key":"356_CR23","unstructured":"ISO\/IEC\/IEEE 29119-2:2013(e): Software and systems engineering\u2014software testing\u2014part 2: Test processes. Sept (2013)"},{"key":"356_CR24","doi-asserted-by":"crossref","unstructured":"Kalaji, A.S., Hierons, R.M., Swift, S.: Generating feasible transition paths for testing from an extended finite state machine (efsm). In: ICST, IEEE Computer Society, Silver Spring, pp. 230\u2013239 (2009)","DOI":"10.1109\/ICST.2009.29"},{"key":"356_CR25","unstructured":"Lapschies, F.: SONOLAR homepage. http:\/\/www.informatik.uni-bremen.de\/agbs\/florian\/sonolar\/ . Accessed June 2014"},{"key":"356_CR26","unstructured":"Object Management Group: OMG Systems Modeling Language ( $$\\text{ OMG } \\text{ SysML }^{{TM}}$$ OMG SysML T M ). Technical report, Object Management Group, 2010. OMG Document Number: formal\/2010-06-02 (2010)"},{"key":"356_CR27","unstructured":"Object Management Group: OMG Unified Modeling Language (OMG UML), superstructure, version 2.4.1. Technical report, OMG (2011)"},{"key":"356_CR28","first-page":"53","volume":"19","author":"J Peleska","year":"1997","unstructured":"Peleska, J., Siegel, M.: Test automation of safety\u2013critical reactive systems. S. Afr. Comput. J. 19, 53\u201377 (1997)","journal-title":"S. Afr. Comput. J."},{"key":"356_CR29","doi-asserted-by":"crossref","unstructured":"Peleska, J.: Industrial-strength model-based testing\u2014state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, Rome, Italy, 17th March 2013. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"356_CR30","doi-asserted-by":"crossref","unstructured":"Peleska, J., Honisch, A., Lapschies, F., L\u00f6ding, H., Schmid, H., Smuda, P., Vorobev, E., Zahlten, C.: A real-world benchmark model for testing concurrent real-time systems in the automotive domain. In: Wolff, B., Zaidi, F. (eds.) Testing Software and Systems. Proceedings of the 23rd IFIP WG 6.1 International Conference, ICTSS 2011. LNCS, vol. 7019, pp. 146\u2013161, Nov 2011. IFIP WG 6.1, Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24580-0_11"},{"key":"356_CR31","doi-asserted-by":"crossref","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) Nasa Formal Methods. Third International Symposium, NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"356_CR32","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-0-387-35079-0_10","volume-title":"Formal description techniques IX\u2014theory, application and tools","author":"A Petrenko","year":"1996","unstructured":"Petrenko, A., Yevtushenko, N., Bochmann, G.v: Fault models for testing in context. In: Gotzhein, Reinhard, Bredereke, Jan (eds.) Formal description techniques IX\u2014theory, application and tools, pp. 163\u2013177. Chapman & Hall, London (1996)"},{"issue":"4","key":"356_CR33","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/s10009-012-0240-3","volume":"14","author":"A Petrenko","year":"2012","unstructured":"Petrenko, A., Simao, A., Maldonado, J.C.: Model-based testing of software and systems: recent advances and challenges. Int. J. Softw. Tools Technol. Transf. 14(4), 383\u2013386 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"6","key":"356_CR34","first-page":"71","volume":"21","author":"S Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. IEEE Mag. Intell. Syst. Trends Controv. 21(6), 71\u201381 (2006)","journal-title":"IEEE Mag. Intell. Syst. Trends Controv."},{"key":"356_CR35","unstructured":"RTCA, SC-167 Software Considerations in Airborne Systems and Equipment Certification, RTCA\/DO-178B RTCA (1992)"},{"key":"356_CR36","volume-title":"Software testing foundations","author":"A Spillner","year":"2006","unstructured":"Spillner, A., Linz, T., Schaefer, H.: Software testing foundations. Dpunkt.verlag, Heidelberg (2006)"},{"issue":"1\u20132","key":"356_CR37","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/S0304-3975(99)00134-6","volume":"254","author":"JG Springintveld","year":"2001","unstructured":"Springintveld, J.G., Vaandrager, F.W., D\u2019Argenio, P.R.: Testing timed automata. Theor. Comput. Sci. 254(1\u20132), 225\u2013257 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"356_CR38","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0169-7552(96)00017-7","volume":"29","author":"J Tretmans","year":"1996","unstructured":"Tretmans, J.: Conformance testing with labelled transition systems: implementation relations and test generation. Comput. Netw. ISDN Syst. 29(1), 49\u201379 (1996)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"356_CR39","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. Lecture Notes in Computer Science, vol. 4949, pp. 1\u201338. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"356_CR40","unstructured":"UNISIG: ERTMS\/ETCS System Requirements Specification, chap. 3. Principles, vol. Subset-026-3, chapt. 3. Issue 3.3.0 (2012)"},{"key":"356_CR41","first-page":"98","volume":"4","author":"MP Vasilevskii","year":"1973","unstructured":"Vasilevskii, M.P.: Failure diagnosis of automata. Kibernetika (Transl.) 4, 98\u2013108 (1973)","journal-title":"Kibernetika (Transl.)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0356-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0356-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0356-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T17:17:38Z","timestamp":1566062258000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0356-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,21]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["356"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0356-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,21]]}}}