{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T08:10:02Z","timestamp":1748765402262,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"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-29613-5_3","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T07:47:34Z","timestamp":1453967254000},"page":"40-60","source":"Crossref","is-referenced-by-count":1,"title":["Testing the IPC Protocol for a Real-Time Operating System"],"prefix":"10.1007","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[]},{"given":"Oto","family":"Havle","sequence":"additional","affiliation":[]},{"given":"Yakoub","family":"Nemouchi","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods and Testing","year":"2008","unstructured":"Hierons, R.M., Bowen, J.P., Harman, M. (eds.): FORTEST. LNCS, vol. 4949. Springer, Heidelberg (2008)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73770-4_9","volume-title":"Tests and Proofs","author":"AD Brucker","year":"2007","unstructured":"Brucker, A.D., Wolff, B.: Test-sequence generation with Hol-TestGen with an application to firewall testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 149\u2013168. Springer, Heidelberg (2007)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-00593-0_28","volume-title":"Fundamental Approaches to Software Engineering","author":"AD Brucker","year":"2009","unstructured":"Brucker, A.D., Wolff, B.: hol-TestGen: an interactive test-case generation framework. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 417\u2013420. Springer, Heidelberg (2009)"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-012-0222-y","volume":"25","author":"AD Brucker","year":"2012","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects Comput. 25, 683\u2013721 (2012)","journal-title":"Formal Aspects Comput."},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-38916-0_5","volume-title":"Tests and Proofs","author":"AD Brucker","year":"2013","unstructured":"Brucker, A.D., Feliachi, A., Nemouchi, Y., Wolff, B.: Test program generation for a microprocessor. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 76\u201395. Springer, Heidelberg (2013)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-30473-6_8","volume-title":"Tests and Proofs","author":"H Ponce de Le\u00f3n","year":"2012","unstructured":"Ponce de Le\u00f3n, H., Haar, S., Longuet, D.: Conformance relations for labeled event structures. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 83\u201398. Springer, Heidelberg (2012)"},{"key":"3_CR7","unstructured":"Euro-Mils. http:\/\/www.euromils.eu\/"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-41202-8_10","volume-title":"Formal Methods and Software Engineering","author":"A Feliachi","year":"2013","unstructured":"Feliachi, A., Gaudel, M.-C., Wenzel, M., Wolff, B.: The $$Circus$$ C i r c u s testing theory revisited in Isabelle\/HOL. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 131\u2013147. Springer, Heidelberg (2013)"},{"key":"3_CR9","volume-title":"Introduction to the Theory of Finite-State Machines","author":"A Gill","year":"1962","unstructured":"Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"H\u00e4rtig, H., Hohmuth, M., Liedtke, J., Sch\u00f6nberg, S., Wolter, J.: The performance of microkernel-based systems. In: SOSP (1997)","DOI":"10.1145\/268998.266660"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"5","key":"3_CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/224056.224075","volume":"29","author":"J Liedtke","year":"1995","unstructured":"Liedtke, J.: On $$\\mu $$ \u03bc -kernel construction. SOSP 29(5), 237\u2013250 (1995)","journal-title":"SOSP"},{"issue":"3","key":"3_CR13","first-page":"219","volume":"2","author":"N Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI-Quart. 2(3), 219\u2013246 (1989)","journal-title":"CWI-Quart."},{"key":"3_CR14","unstructured":"Common criteria for information technology security evaluation. http:\/\/www.commoncriteriaportal.org\/"},{"key":"3_CR15","unstructured":"Musuvathi, M., Qadeer, S., Ball, T.: Chess: a systematic testing tool for concurrent software. Technical report MSR-TR-2007-149, Microsoft Research (2007)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Shan Lu, W.J., Zhou, Y.: A study of interleaving coverage criteria. In: ESEC-FSE Companion, pp. 533\u2013536 (2007)","DOI":"10.1145\/1295014.1295034"},{"key":"3_CR18","unstructured":"SYSGO: Pikeos. http:\/\/www.sysgo.com\/products\/pikeos-rtos-and-virtualization-concept\/"},{"key":"3_CR19","unstructured":"SYSGO: PikeOS Fundamentals. SYSGO (2013)"},{"key":"3_CR20","unstructured":"SYSGO: PikeOS Kernel. SYSGO (2013)"},{"key":"3_CR21","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: An Outcome of the FORTEST Network","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. 4949, pp. 1\u201338. Springer, Heidelberg (2008)"},{"issue":"4","key":"3_CR22","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2(4), 461\u2013493 (1992)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"3_CR23","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1145\/267580.267590","volume":"29","author":"H Zhu","year":"1997","unstructured":"Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. (CSUR) 29(4), 366\u2013427 (1997)","journal-title":"ACM Comput. Surv. (CSUR)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T07:33:21Z","timestamp":1748763201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}