{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T10:40:02Z","timestamp":1748688002438,"version":"3.41.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259444"},{"type":"electronic","value":"9783319259451"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25945-1_1","type":"book-chapter","created":{"date-parts":[[2015,11,7]],"date-time":"2015-11-07T03:20:37Z","timestamp":1446866437000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Checking Experiments for Finite State Machines with Symbolic Inputs"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Petrenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adenilso","family":"Simao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"issue":"8","key":"1_CR1","doi-asserted-by":"publisher","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","volume":"86","author":"S Anand","year":"2013","unstructured":"Anand, S., Burke, E.K., Chen, T.Y., Clark, J., Cohen, M.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":"1_CR2","unstructured":"Bochmann, G.V., Das, A., Dssouli, R., Dubuc, M., Ghedamsi, A., Luo, G.: Fault models in testing. In: Proceedings of the IFIP TC6\/WG6. 1 Fourth International Workshop on Protocol Test Systems, IV, pp. 17\u201330. North-Holland Publishing Co. (1991)"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Cheng, K.T., Krishnakumar, A.S.: Automatic functional test generation using the extended finite state machine model. In: Proceedings of the 30th Design Automation Conference, pp. 86\u201391 (1993)","DOI":"10.1145\/157485.164585"},{"issue":"3","key":"1_CR4","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"TS Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Software Eng. 4(3), 178\u2013187 (1978)","journal-title":"IEEE Trans. Software Eng."},{"key":"1_CR5","unstructured":"Chun, W., Amer, P.D.L.: Test case generation for protocols specified in Estelle. In: Proceedings of the IFIP TC6\/WG6. 1 Third International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, III, pp. 191\u2013206. North-Holland Publishing Co. (1990)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Dorofeeva, R., Yevtushenko, N., El-Fakih, K. and Cavalli, A.: Experimental evaluation of FSM-based testing methods. In: Third IEEE International Conference Software Engineering and Formal Methods, pp. 23\u201332. IEEE Computer Society (2005)","DOI":"10.1109\/SEFM.2005.17"},{"key":"1_CR7","unstructured":"European Railway Agency: ERTMS\u2014System Requirements Specification\u2014UNISIG SUBSET-026, May 2014. http:\/\/www.era.europa.eu\/Document-Register\/Pages\/Set-2-System-Requirements-Specification.aspx"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31848-4_1","volume-title":"Formal Approaches to Software Testing","author":"L Frantzen","year":"2005","unstructured":"Frantzen, L., Tretmans, J., Willemse, T.A.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 1\u201315. Springer, Heidelberg (2005)"},{"key":"1_CR9","volume-title":"A Practical Guide to SysML: the Systems Modeling Language","author":"S Friedenthal","year":"2014","unstructured":"Friedenthal, S., Moore, A., Steiner, R.: A Practical Guide to SysML: the Systems Modeling Language. Morgan Kaufmann, San Francisco (2014)"},{"issue":"6","key":"1_CR10","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1109\/32.87284","volume":"17","author":"S Fujiwara","year":"1991","unstructured":"Fujiwara, S., von 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."},{"issue":"3","key":"1_CR11","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/S1389-1286(03)00247-0","volume":"42","author":"U Gl\u00e4sser","year":"2003","unstructured":"Gl\u00e4sser, U., Gotzhein, R., Prinz, A.: The formal semantics of SDL-2000: status and perspectives. Comput. Netw. 42(3), 343\u2013358 (2003)","journal-title":"Comput. Netw."},{"issue":"4","key":"1_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Hennie, F.C.: Fault-detecting experiments for sequential circuits. In: Proceedings of the Fifth Annual Symposium on Circuit Theory and Logical Design, pp. 95\u2013110 (1965)","DOI":"10.1109\/SWCT.1964.8"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-46002-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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 2002. LNCS, vol. 2280, pp. 327\u2013341. Springer, Heidelberg (2002)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-41707-8_4","volume-title":"Testing Software and Systems","author":"W-l Huang","year":"2013","unstructured":"Huang, W.-l., Peleska, J.: Exhaustive model-based equivalence class testing. In: Yenig\u00fcn, H., Yilmaz, C., Ulrich, A. (eds.) ICTSS 2013. LNCS, vol. 8254, pp. 49\u201364. Springer, Heidelberg (2013)"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Huang, W., Peleska, J.: Complete model-based equivalence class testing. Int. J. Softw. Tools Technol. Transf. (2014). doi: 10.1007\/s10009-014-0356-8","DOI":"10.1007\/s10009-014-0356-8"},{"key":"1_CR17","unstructured":"J\u00e9ron, T., Veanes, M., Wolff, B. (eds.) Symbolic methods in testing. Report from Dagstuhl Seminar 13021 (2013)"},{"key":"1_CR18","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: International Conference on Software Testing, Verification and Validation, pp. 230\u2013239. IEEE Computer Society, Silver Spring (2009)","DOI":"10.1109\/ICST.2009.29"},{"key":"1_CR19","series-title":"IFIP","first-page":"225","volume-title":"Protocol Test Systems","author":"X Li","year":"1994","unstructured":"Li, X., Higashino, T., Higuchi, M., Taniguchi, K.: Automatic generation of extended UIO sequences for communication protocols in an EFSM model. In: Mizuno, T., Higashino, T., Shiratori, N. (eds.) Protocol Test Systems. IFIP, pp. 225\u2013240. Springer, New York (1994)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-54862-8_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Maler","year":"2014","unstructured":"Maler, O., Mens, I.-E.: Learning regular languages over large alphabets. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 485\u2013499. Springer, Heidelberg (2014)"},{"key":"1_CR21","series-title":"Automata Studies","first-page":"129","volume-title":"Gedanken-experiments on sequential machines","author":"EF Moore","year":"1956","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. Automata Studies, pp. 129\u2013153. Princeton University Press, Princeton (1956)"},{"key":"1_CR22","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 de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"3","key":"1_CR23","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1012291501330","volume":"4","author":"G Noord van","year":"2001","unstructured":"van Noord, G., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4(3), 263\u2013286 (2001)","journal-title":"Grammars"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Petrenko, A., Yevtushenko, N.: Test suite generation for a given type of implementation errors. In: Proceedings of the IFIP XII International Conference Protocol Specification, Testing, and Verification, pp. 229\u2013243 (1992)","DOI":"10.1016\/B978-0-444-89874-6.50021-0"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Petrenko, A., Yevtushenko, N., von Bochmann, G.: Fault models for testing in context. In: Formal Description Techniques IX\u2014Theory, Application and Tools, pp. 163\u2013177. Chapman & Hall, London (1996)","DOI":"10.1007\/978-0-387-35079-0_10"},{"issue":"1","key":"1_CR26","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/TSE.2004.1265734","volume":"30","author":"A Petrenko","year":"2004","unstructured":"Petrenko, A., Boroday, S., Groz, R.: Confirming configurations in EFSM testing. IEEE Trans. Softw. Eng. 30(1), 29\u201342 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/11759744_9","volume-title":"Formal Approaches to Software Testing","author":"A Petrenko","year":"2006","unstructured":"Petrenko, A., Yevtushenko, N.: Conformance tests as checking experiments for partial nondeterministic FSM. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 118\u2013133. Springer, Heidelberg (2006)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Petrenko, A., Dury, A., Ramesh, S., Mohalik, S.: A method and tool for test optimization for automotive controllers. In: Proceedings of the 9th Workshop on Advances in Model Based Testing (A-MOST 2013) of the 6th IEEE International Conference on Software Testing, Verification and Validation (ICST 2013), Luxembourg (2013)","DOI":"10.1109\/ICSTW.2013.31"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-40911-4_20","volume-title":"Integrated Formal Methods","author":"V Rusu","year":"2000","unstructured":"Rusu, V., du Bousquet, L., J\u00e9ron, T.: An approach to symbolic test generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 338\u2013357. Springer, Heidelberg (2000)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-05031-2_9","volume-title":"Testing of Software and Communication Systems","author":"A Simao","year":"2009","unstructured":"Simao, A., Petrenko, A., Yevtushenko, N.: Generating Reduced Tests for FSMs with Extra States. In: N\u00fa\u00f1ez, M., Baker, P., Merayo, M.G. (eds.) TESTCOM 2009. LNCS, vol. 5826, pp. 129\u2013145. Springer, Heidelberg (2009)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Simao, A., Petrenko, A.: Generating complete and finite test suite for ioco: is it possible? In: Proceedings of MBT 2014, Electronic Proceedings in Theoretical Computer Science, vol. 141, pp. 56\u201370 (2014)","DOI":"10.4204\/EPTCS.141.5"},{"key":"1_CR32","unstructured":"Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International (2002)"},{"issue":"4","key":"1_CR33","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/BF01068590","volume":"9","author":"MP Vasilevskii","year":"1973","unstructured":"Vasilevskii, M.P.: Failure diagnosis of automata. Cybernetics 9(4), 653\u2013665 (1973). Plenum Publishing Corporation, New York","journal-title":"Cybernetics"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Implementation and Application of Automata","author":"Margus Veanes","year":"2013","unstructured":"Veanes, Margus: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16\u201323. Springer, Heidelberg (2013)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: algorithms and applications. In: Proceedings of the 39th ACM Symposium on Principles of programming languages, pp. 137\u2013150 (2012)","DOI":"10.1145\/2103656.2103674"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Wang, C.J., Liu, M.T.: Generating test cases for EFSM with given fault model. In: Proceedings of Twelfth Conference of the IEEE Computer and Communications Societies, pp. 774\u2013781 (1993)","DOI":"10.1109\/INFCOM.1993.253292"},{"key":"1_CR37","unstructured":"Watson, B.W.: Implementing and using finite automata toolkits. In: Extended Finite State Models of Language, pp. 19\u201336. Cambridge University Press, New York (1999)"},{"issue":"2","key":"1_CR38","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1006\/jcss.1995.1019","volume":"50","author":"M Yannakakis","year":"1995","unstructured":"Yannakakis, M., Lee, D.: Testing finite state machines: fault detection. J. Comput. Syst. Sci. 50(2), 209\u2013227 (1995)","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"1_CR39","first-page":"50","volume":"24","author":"N Yevtushenko","year":"1990","unstructured":"Yevtushenko, N., Petrenko, A.: Synthesis of test experiments in some classes of automata. Autom. Control Comput. Sci. 24(4), 50\u201355 (1990)","journal-title":"Autom. Control Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25945-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T10:24:05Z","timestamp":1748687045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25945-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259444","9783319259451"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25945-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}