{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T04:16:30Z","timestamp":1749701790097,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_1","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"3-22","source":"Crossref","is-referenced-by-count":5,"title":["Industrial-Strength Model-Based Testing of Safety-Critical Systems"],"prefix":"10.1007","author":[{"given":"Jan","family":"Peleska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen-ling","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"issue":"8","key":"1_CR1","doi-asserted-by":"crossref","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.A., 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","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"5","key":"1_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods Comput. Sci. 2(5), 1\u201364 (2006). arXiv:cs\/0611029","journal-title":"Logical Methods Comput. Sci."},{"key":"1_CR4","unstructured":"von Bochmann, G., Das, A., Dssouli, R., Dubuc, M., Ghedamsi, A., Luo, G.: Fault models in testing. In: Kroon, J., Heijink, R.J., Brinksma, E. (eds.) Proceedings of the IFIP TC6\/WG6.1 Fourth International Workshop on Protocol Test Systems IV, 15\u201317 October 1991, Leidschendam, The Netherlands, pp. 17\u201330. North-Holland (1991). IFIP Transactions, vol. C-3"},{"key":"1_CR5","unstructured":"CENELEC: EN 50128: 2011 Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems (2011)"},{"issue":"3","key":"1_CR6","doi-asserted-by":"crossref","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. Softw. Eng. SE 4(3), 178\u2013186 (1978)","journal-title":"IEEE Trans. Softw. Eng. SE"},{"key":"1_CR7","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":"1_CR8","volume-title":"Algebraic Theory of Processes","author":"M Hennessy","year":"1988","unstructured":"Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)"},{"issue":"10","key":"1_CR9","doi-asserted-by":"crossref","first-page":"1330","DOI":"10.1109\/TC.2004.85","volume":"53","author":"RM Hierons","year":"2004","unstructured":"Hierons, R.M.: Testing from a nondeterministic finite state machine using adaptive state counting. IEEE Trans. Comput. 53(10), 1330\u20131342 (2004). http:\/\/doi.ieeecomputersociety.org\/10.1109\/TC.2004.85","journal-title":"IEEE Trans. Comput."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Huang, W., Peleska, J.: Complete model-based equivalence class testing for nondeterministic systems. Formal Aspects of Computing Under review","DOI":"10.1007\/s00165-016-0402-2"},{"issue":"3","key":"1_CR11","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s10009-014-0356-8","volume":"18","author":"W Huang","year":"2016","unstructured":"Huang, W., Peleska, J.: Complete model-based equivalence class testing. STTT 18(3), 265\u2013283 (2016). http:\/\/dx.doi.org\/10.1007\/s10009-014-0356-8","journal-title":"STTT"},{"key":"1_CR12","unstructured":"Huang, W.l., Peleska, J., Schulze, U.: Test automation support. Technical report D34.1, COMPASS Comprehensive Modelling for Advanced Systems of Systems (2013). http:\/\/www.compass-research.eu\/deliverables.html"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-21215-9_10","volume-title":"Tests and Proofs","author":"F H\u00fcbner","year":"2015","unstructured":"H\u00fcbner, F., Huang, W., Peleska, J.: Experimental evaluation of a novel equivalence class partition testing strategy. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 155\u2013172. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21215-9_10"},{"key":"1_CR14","unstructured":"ISO, DIS 26262\u20134: Road vehicles - functional safety - part 4: Product development: system level. Technical report, International Organization for Standardization (2009)"},{"key":"1_CR15","unstructured":"ISO, IEC, IEEE DIS 29119\u20134.2: Software and systems engineering - software testing - part: 4 test techniques, February 2014"},{"issue":"2","key":"1_CR16","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1109\/32.265636","volume":"20","author":"G Luo","year":"1994","unstructured":"Luo, G., von Bochmann, G., Petrenko, A.: Test selection based on communicating nondeterministic finite-state machines using a generalized WP-method. IEEE Trans. Softw. Eng. 20(2), 149\u2013162 (1994). http:\/\/doi.ieeecomputersociety.org\/10.1109\/32.265636","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"8","key":"1_CR17","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1109\/32.57623","volume":"16","author":"LJ Morell","year":"1990","unstructured":"Morell, L.J.: A theory of fault-based testing. IEEE Trans. Softw. Eng. 16(8), 844\u2013857 (1990). http:\/\/dx.doi.org\/10.1109\/32.57623","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR18","unstructured":"Object Management Group: Object Constraint Language, Version 2.4. Technical report, Object Management Group (2014). http:\/\/www.omg.org\/spec\/OCL\/2.4\/"},{"key":"1_CR19","unstructured":"Object Management Group: OMG Systems Modeling Language (OMG SysML), Version 1.4. Technical report, Object Management Group (2015). http:\/\/www.omg.org\/spec\/SysML\/1.4"},{"key":"1_CR20","unstructured":"Peleska, J.: Formal methods and the development of dependable systems. No. 9612, Christian-Albrechts-Universit\u00e4t Kiel, Institut fr Informatik und Praktische Mathematik , Habilitationsschrift, December 1996"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Peleska, J.: Industrial-strength model-based testing-state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing. Electronic Proceedings in Theoretical Computer Science, 17th March 2013, Rome, Italy, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-24580-0_11","volume-title":"Testing Software and Systems","author":"J Peleska","year":"2011","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., Za\u00efdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 146\u2013161. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24580-0_11"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-45943-1_1","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"J Peleska","year":"2016","unstructured":"Peleska, J., Huang, W.: Model-based testing strategies and their (in)dependence on syntactic model representations. In: Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS\/AVoCS -2016. LNCS, vol. 9933, pp. 3\u201321. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-45943-1_1"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-33951-1_3","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"J Peleska","year":"2016","unstructured":"Peleska, J., Huang, W., H\u00fcbner, F.: A novel approach to HW\/SW integration testing of route-based interlocking system controllers. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 32\u201349. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-33951-1_3"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J Peleska","year":"2011","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.) NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_22"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-24580-0_12","volume-title":"Testing Software and Systems","author":"A Petrenko","year":"2011","unstructured":"Petrenko, A., Yevtushenko, N.: Adaptive testing of deterministic implementations specified by nondeterministic FSMs. In: Wolff, B., Za\u00efdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 162\u2013178. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24580-0_12"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Petrenko, A., Yevtushenko, N., Bochmann, G.v.: Fault models for testing in context. In: Gotzhein, R., Bredereke, J. (eds.) Formal Description Techniques IX - Theory, Application and Tools, pp. 163\u2013177. Chapman & Hall (1996)","DOI":"10.1007\/978-0-387-35079-0_10"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Petrenko, A., Yevtushenko, N., Bochmann, G.V.: Testing deterministic implementations from nondeterministic FSM specifications. In: IFIP TC6 9th International Workshop on Testing of Communicating Systems, pp. 125\u2013141. Chapman and Hall (1996)","DOI":"10.1007\/978-0-387-35062-2_10"},{"issue":"4","key":"1_CR29","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). http:\/\/dx.doi.org\/10.1007\/s10009-012-0240-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Pretschner, A.: Defect-based testing. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 224\u2013245. IOS Press (2015). http:\/\/dx.doi.org\/10.3233\/978-1-61499-495-4-224","DOI":"10.3233\/978-1-61499-495-4-224"},{"issue":"5","key":"1_CR31","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Asp. Comput. 6(5), 495\u2013512 (1994). http:\/\/dx.doi.org\/10.1007\/BF01211865","journal-title":"Formal Asp. Comput."},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-02674-4_14","volume-title":"Model Driven Architecture - Foundations and Applications","author":"M Soden","year":"2009","unstructured":"Soden, M., Eichler, H.: Temporal extensions of OCL revisited. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 190\u2013205. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02674-4_14"},{"issue":"1","key":"1_CR33","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."},{"issue":"5","key":"1_CR34","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1002\/stvr.456","volume":"22","author":"M Utting","year":"2012","unstructured":"Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297\u2013312 (2012). http:\/\/dx.doi.org\/10.1002\/stvr.456","journal-title":"Softw. Test. Verif. Reliab."},{"key":"1_CR35","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.)"},{"key":"1_CR36","unstructured":"WG-71, R.S.E.: Software Considerations in Airborne Systems and Equipment Certification. Technical report RTCA\/DO-178C, RTCA Inc., 1140 Connecticut Avenue, N.W., Suite 1020, Washington, D.C. 20036, December 2011"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:24:15Z","timestamp":1749691455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}