{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T11:24:43Z","timestamp":1769599483803,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642389153","type":"print"},{"value":"9783642389160","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38916-0_2","type":"book-chapter","created":{"date-parts":[[2013,6,10]],"date-time":"2013-06-10T02:13:47Z","timestamp":1370830427000},"page":"20-38","source":"Crossref","is-referenced-by-count":53,"title":["Time for Mutants \u2014 Model-Based Mutation Testing with Timed Automata"],"prefix":"10.1007","author":[{"given":"Bernhard K.","family":"Aichernig","sequence":"first","affiliation":[]},{"given":"Florian","family":"Lorber","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Brandl, H., J\u00f6bstl, E., Krenn, W.: Efficient mutation killers in action. In: ICST, pp. 120\u2013129 (2011)","DOI":"10.1109\/ICST.2011.57"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1921532.1921559","volume":"36","author":"B.K. Aichernig","year":"2011","unstructured":"Aichernig, B.K., Brandl, H., J\u00f6bstl, E., Krenn, W.: UML in action: a two-layered interpretation for testing. ACM SIGSOFT SEN\u00a036(1), 1\u20138 (2011)","journal-title":"ACM SIGSOFT SEN"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-36135-9_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 243\u2013259. Springer, Heidelberg (2002)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-24310-3_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B. Badban","year":"2011","unstructured":"Badban, B., Lange, M.: Exact incremental analysis of timed automata with an SMT-solver. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.\u00a06919, pp. 177\u2013192. Springer, Heidelberg (2011)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Belli, F., Budnik, C.J., Wong, W.E.: Basic operations for generating behavioral mutants. In: MUTATION, pp. 9\u201318. IEEE Computer Society Press (2006)","DOI":"10.1109\/MUTATION.2006.2"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 117\u2013148 (2003)","journal-title":"Advances in Computers"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Boroday, S., Petrenko, A., Groz, R.: Can a model checker generate tests for non-deterministic systems? ENTCS\u00a0190(2), 3\u201319 (2007); MBT 2007","DOI":"10.1016\/j.entcs.2007.08.002"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-17071-3_11","volume-title":"Formal Methods for Components and Objects","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., R\u00fcmmer, P., Weissenbacher, G.: Mutation-based test case generation for simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 208\u2013227. Springer, Heidelberg (2010)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-31848-4_5","volume-title":"Formal Approaches to Software Testing","author":"L.B. Briones","year":"2005","unstructured":"Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol.\u00a03395, pp. 64\u201378. Springer, Heidelberg (2005)"},{"key":"2_CR11","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: LICS, pp. 428\u2013439 (1990)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Engeler, E. (ed.) Logic of Programs 1979. LNCS, vol.\u00a0125, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G. Fraser","year":"2009","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab.\u00a019(3), 215\u2013261 (2009)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"He, N., R\u00fcmmer, P., Kroening, D.: Test-case generation for embedded simulink via formal concept analysis. In: DAC, pp. 224\u2013229 (2011)","DOI":"10.1145\/2024724.2024777"},{"issue":"5","key":"2_CR16","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 Transactions on Software Engineering\u00a037(5), 649\u2013678 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"2_CR17","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10703-009-0065-1","volume":"34","author":"M. Krichen","year":"2009","unstructured":"Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design\u00a034(3), 238\u2013304 (2009)","journal-title":"Formal Methods in System Design"},{"issue":"1-2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT\u00a01(1-2), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"2_CR19","unstructured":"Mikucionis, M., Larsen, K.G., Nielsen, B.: T-uppaal: Online model-based testing of real-time systems. In: ASE, pp. 396\u2013397 (2004)"},{"key":"2_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 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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45739-9_15","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P. Niebert","year":"2002","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 225\u2013244. Springer, Heidelberg (2002)"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10009-002-0094-1","volume":"5","author":"B. Nielsen","year":"2003","unstructured":"Nielsen, B., Skou, A.: Automated test generation from timed automata. STTT\u00a05(1), 59\u201377 (2003)","journal-title":"STTT"},{"key":"2_CR23","unstructured":"Nilsson, R., Offutt, J., Andler, S.F.: Mutation-based testing criteria for timeliness. In: COMPSAC 2004, vol.\u00a01, pp. 306\u2013311 (2004)"},{"issue":"4","key":"2_CR24","first-page":"97","volume":"164","author":"R. Nilsson","year":"2006","unstructured":"Nilsson, R., Offutt, J., Mellin, J.: Test case generation for mutation-based testing of timeliness. ENTCS\u00a0164(4), 97\u2013114 (2006); MBT 2006","journal-title":"ENTCS"},{"key":"2_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.\u00a06617, pp. 298\u2013312. Springer, Heidelberg (2011)"},{"key":"2_CR26","unstructured":"Fabbri, S.C.P.F., Delamaro, M.E., Maldonado, J.C., Masiero, P.C.: Mutation analysis testing for finite state machines. In: ICSRE, pp. 220\u2013229 (1994)"},{"key":"2_CR27","unstructured":"Fabbri, S.C.P.F., Maldonado, J.C., Sugeta, T., Masiero, P.C.: Mutation testing applied to validate specifications based on statecharts. In: Software Reliability Engineering, pp. 210\u2013219 (1999)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Queille, J., Sifakis, J.: Iterative methods for the analysis of petri nets. In: Selected Papers from the First and the Second European Workshop on ICATPN, pp. 161\u2013167 (1981)","DOI":"10.1007\/978-3-642-68353-4_27"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-24270-0_20","volume-title":"Computer Safety, Reliability, and Security","author":"R. Schlick","year":"2011","unstructured":"Schlick, R., Herzner, W., J\u00f6bstl, E.: Fault-based generation of test cases from UML-models - approach and some experiences. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol.\u00a06894, pp. 270\u2013283. Springer, Heidelberg (2011)"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-85778-5_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J. Schmaltz","year":"2008","unstructured":"Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 250\u2013264. Springer, Heidelberg (2008)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing","author":"J. Tretmans","year":"2008","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol.\u00a04949, pp. 1\u201338. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38916-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:19:55Z","timestamp":1557793195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38916-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389153","9783642389160"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38916-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}