{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:35:33Z","timestamp":1725539733686},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642332951"},{"type":"electronic","value":"9783642332968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33296-8_11","type":"book-chapter","created":{"date-parts":[[2012,9,16]],"date-time":"2012-09-16T22:24:55Z","timestamp":1347834295000},"page":"131-146","source":"Crossref","is-referenced-by-count":5,"title":["Investigating Time Properties of Interrupt-Driven Programs"],"prefix":"10.1007","author":[{"given":"Yanhong","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianqi","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Huang, Y., He, J., Liu, S.: Formal Model of Interrupt Program from a Probabilistic Perspective. In: ICECCS (2011)","DOI":"10.1109\/ICECCS.2011.16"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Regehra, J., Coopridera, N.: Interrupt Verification via Thread Verification. ENTCS (2007)","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Regehra, J.: Random testing of interrupt-driven software. ACM (2005)","DOI":"10.1145\/1086228.1086282"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Kleiman, S., Eykholt, J.: Interrupts as threads. In: ACM SIGOPS (1995)","DOI":"10.1145\/202213.202217"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reasoning\u00a042(2-4) (2009)","DOI":"10.1007\/s10817-009-9118-9"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Hills, T.: Structured interrupts. In: ACM SIGOPS (1993)","DOI":"10.1145\/160551.160556"},{"key":"11_CR7","unstructured":"Cobben, T., Engels, A.: Interrupt and Disrupt in MSC: Possibilities and Problems (1998)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Syntax and Defining equations for an interrupt mechanism in process algebra. In: FIIX (1986)","DOI":"10.3233\/FI-1986-9202"},{"key":"11_CR9","unstructured":"Brylow, D., Damgaard, N., Palsberg, J.: Static Checking of Interrupt-driven Software. In: ICSE (2001)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45739-9_18","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J. Palsberg","year":"2002","unstructured":"Palsberg, J., Ma, D.: A Typed Interrupt Calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 291\u2013310. Springer, Heidelberg (2002)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/3-540-44898-5_7","volume-title":"Static Analysis","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack Size Analysis for Interrupt-driven Programs. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 109\u2013126. Springer, Heidelberg (2003)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-Driven Software. IEEE Transactions on Software Engineering (2004)","DOI":"10.1109\/TSE.2004.64"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Regehra, J.: Handbook of Real-Time and Embedded Systems. In: Safe and Structured Use of Interrupts in Real-Time and Embedded Software (2007)","DOI":"10.1201\/9781420011746.ch16"},{"key":"11_CR14","unstructured":"Kleidermacher, D.: Minimizing Interrupt Response Time, Design Strategies and Methodologies 4(1) (2005)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-75664-4_28","volume-title":"Software Technologies for Embedded and Ubiquitous Systems","author":"J. Jeong","year":"2007","unstructured":"Jeong, J., Seo, E., Kim, D.-S., Kim, J.-S., Lee, J., Jung, Y.-J., Kim, D.-H., Kim, K.: Transparent and Selective Real-Time Interrupt Services for Performance Improvement. In: Obermaisser, R., Nah, Y., Puschner, P., Rammig, F.J. (eds.) SEUS 2007. LNCS, vol.\u00a04761, pp. 283\u2013292. Springer, Heidelberg (2007)"},{"key":"11_CR16","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming, Prentice Hall International Series in Computer Science (1998)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Shi, J., Zhu, L., Huang, Y., Guo, J., Zhu, H., Fang, H., Ye, X.: Binary Code Level Verfication for Interrupt Safety Properties of Real-Time Operating System. In: TASE (2012)","DOI":"10.1109\/TASE.2012.46"},{"key":"11_CR18","unstructured":"Milner, R.: Communication and Comcurrency. Prentice Hall International Series in Computer Science (1990)"},{"key":"11_CR19","unstructured":"Milner, R.: Communication and Mobile System: \u03c0\u2009\u2212 caculus. Cambirdge University Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33296-8_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,29]],"date-time":"2022-01-29T01:58:32Z","timestamp":1643421512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33296-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642332951","9783642332968"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33296-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}