{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:23:23Z","timestamp":1762521803711,"version":"3.41.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319212142"},{"type":"electronic","value":"9783319212159"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21215-9_4","type":"book-chapter","created":{"date-parts":[[2015,7,16]],"date-time":"2015-07-16T13:36:34Z","timestamp":1437053794000},"page":"58-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Case Study: Automatic Test Case Generation for a Secure Cache Implementation"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Hein","sequence":"additional","affiliation":[]},{"given":"Franz","family":"R\u00f6ck","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Schumi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,17]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing, 1st edn. Cambridge University Press, New York (2008)","edition":"1"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ammann, P., Offutt, J., Huang, H.: Coverage criteria for logical expressions. In: 14th International Symposium on Software Reliability Engineering: ISSRE 2003, pp. 99\u2013107. IEEE (2003)","DOI":"10.1109\/ISSRE.2003.1251034"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bernot, G., Gaudel, M.C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387\u2013405 (1991). http:\/\/dx.doi.org\/10.1049\/sej.1991.0040","DOI":"10.1049\/sej.1991.0040"},{"key":"4_CR4","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proceedings of the 26th International Conference on Software Engineering, ICSE 2004, pp. 326\u2013335. IEEE Computer Society, Washington, DC (2004). http:\/\/dl.acm.org\/citation.cfm?id=998675.999437"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., R\u00f6ck, F., Tautschnig, M.: Automating test-suite augmentation. In: 2014 14th International Conference on Quality Software, October 2\u20133, Allen, TX, USA, pp. 67\u201372 (2014). http:\/\/dx.doi.org\/10.1109\/QSIC.2014.40","DOI":"10.1109\/QSIC.2014.40"},{"key":"4_CR6","unstructured":"Bloem, R.P., Greimel, K., K\u00f6nighofer, R., R\u00f6ck, F.: Model-based MCDC testing of complex decisions for the java card applet firewall. In: VALID Proceedings, IARIA, Ed., pp. 1\u20136 (2013)"},{"issue":"4","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0895-7177(96)00103-3","volume":"24","author":"RJ Brooks","year":"1996","unstructured":"Brooks, R.J., Tobias, A.M.: Choosing the best model: Level of detail, complexity, and model performance. Mathematical and Computer Modelling 24(4), 1\u201314 (1996)","journal-title":"Mathematical and Computer Modelling"},{"key":"4_CR8","unstructured":"Chilenski, J.J.: An investigation of three forms of the modified condition decision coverage (MCDC) criterion. Tech. Rep., DTIC Document (2001)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"4_CR10","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001). http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dalal, S.R., Jain, A., Karunanithi, N., Leaton, J.M., Lott, C.M., Patton, G.C., Horowitz, B.M.: Model-based testing in practice. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 285\u2013294. ACM, New York (1999). http:\/\/doi.acm.org\/10.1145\/302405.302640","DOI":"10.1145\/302405.302640"},{"key":"4_CR12","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 de Moura","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)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: Help for the practicing programmer. Computer 11(4), 34\u201341 (1978). http:\/\/dx.doi.org\/10.1109\/C-M.1978.218136","DOI":"10.1109\/C-M.1978.218136"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME \u201993: Industrial-Strength Formal Methods","author":"J Dick","year":"1993","unstructured":"Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Wing, J.M. (eds.) FME 1993. LNCS, vol. 670, pp. 268\u2013284. Springer, Heidelberg (1993)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Fraser, G., Gargantini, A.: An evaluation of model checkers for specification based test case generation. In: ICST 2009, Second International Conference on Software Testing Verification and Validation, April 1\u20134, Denver, Colorado, USA, pp. 41\u201350 (2009). http:\/\/dx.doi.org\/10.1109\/ICST.2009.33","DOI":"10.1109\/ICST.2009.33"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: A survey. Softw. Test. Verif. Reliab. 19(3), 215\u2013261 (2009). http:\/\/dx.doi.org\/10.1002\/stvr.v19:3","DOI":"10.1002\/stvr.402"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. SIGSOFT Softw. Eng. Notes 24(6), 146\u2013162 (1999). http:\/\/doi.acm.org\/10.1145\/318774.318939","DOI":"10.1145\/318774.318939"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-59293-8_188","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"M-C Gaudel","year":"1995","unstructured":"Gaudel, M.-C.: Testing can be formal, too. In: Mosses, P.D., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 82\u201396. Springer, Heidelberg (1995)"},{"key":"4_CR19","doi-asserted-by":"crossref","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). http:\/\/dl.acm.org\/citation.cfm?id=646486.694621","DOI":"10.1007\/3-540-46002-0_23"},{"key":"4_CR20","unstructured":"Jorgensen, P.C.: Software testing - a craftsman\u2019s approach, 3rd edn. Taylor & Francis (2008)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Offutt, A.J., Untch, R.H.: Mutation, : Uniting the orthogonal. In: Wong, W.E. (ed.) Mutation Testing for the New Century, pp. 34\u201344. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-5939-6_7"},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1002\/stvr.264","volume":"13","author":"J Offutt","year":"2003","unstructured":"Offutt, J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data from state-based specifications. Software Testing, Verification and Reliability 13, 25\u201353 (2003)","journal-title":"Software Testing, Verification and Reliability"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, September 5\u20139, pp. 263\u2013272. ACM, Lisbon (2005). http:\/\/doi.acm.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"4_CR24","doi-asserted-by":"crossref","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","DOI":"10.1002\/stvr.456"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21215-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T08:41:55Z","timestamp":1748508115000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21215-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319212142","9783319212159"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21215-9_4","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":"17 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}