{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T00:16:45Z","timestamp":1694477805973},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,2,3]],"date-time":"2015-02-03T00:00:00Z","timestamp":1422921600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11704-015-3251-x","type":"journal-article","created":{"date-parts":[[2015,2,2]],"date-time":"2015-02-02T20:14:42Z","timestamp":1422908082000},"page":"331-345","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Semantic theories of programs with nested interrupts"],"prefix":"10.1007","volume":"9","author":[{"given":"Yanhong","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","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":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,3]]},"reference":[{"key":"3251_CR1","first-page":"1","volume-title":"Handbook of Real-Time and Embedded Systems, CRC Press","author":"J Regehra","year":"2007","unstructured":"Regehra J. Safe and Structured Use of Interrupts in Real-time and Embedded Software. Handbook of Real-Time and Embedded Systems, CRC Press. 2007, 1\u201315"},{"issue":"2","key":"3251_CR2","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A. A Lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955, 5(2): 285\u2013309","journal-title":"Pacific Journal of Mathematics"},{"key":"3251_CR3","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/160551.160556","volume":"27","author":"T Hills","year":"1993","unstructured":"Hills T. Structured interrupts. ACM SIGOPS Operating Systems Review, 1993, 27: 51\u201368","journal-title":"ACM SIGOPS Operating Systems Review"},{"issue":"9","key":"3251_CR4","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/j.entcs.2007.04.002","volume":"174","author":"J Regehra","year":"2007","unstructured":"Regehra J, Cooprider N. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 2007, 174(9): 139\u2013150","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3251_CR5","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/s10817-009-9118-9","volume":"42","author":"X Feng","year":"2009","unstructured":"Feng X, Shao Z, Guo Y, Dong Y. Certifying low-level programs with hardware interrupts and preemptive threads. Journal of Automated Reasoning, 2009, 42: 301\u2013347","journal-title":"Journal of Automated Reasoning"},{"key":"3251_CR6","doi-asserted-by":"crossref","first-page":"1280","DOI":"10.1109\/49.536480","volume":"14","author":"I Leslie","year":"1996","unstructured":"Leslie I, McAuley D, Black R, Roscoe T, Barham P, Evers D, Fairbairns R, Hyden E. The design and implementation of an operating system to support distributed multimedia applications. IEEE Journal of Selected Areas in Communications, 1996, 14: 1280\u20131297","journal-title":"IEEE Journal of Selected Areas in Communications"},{"key":"3251_CR7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/202213.202217","volume":"29","author":"S Kleiman","year":"1995","unstructured":"Kleiman S, Eykholt J. Interrupts as threads. ACM SIGOPS Operating Systems Review, 1995, 29: 21\u201326","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"3251_CR8","first-page":"47","volume-title":"Proceedings of International Conference on Software Engineering","author":"D Brylow","year":"2001","unstructured":"Brylow D, Damgaard N, Palsberg J. Static checking of interrupt-driven software. In: Proceedings of International Conference on Software Engineering. 2001, 47\u201356"},{"key":"3251_CR9","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/3-540-45739-9_18","volume-title":"Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems","author":"J Palsberg","year":"2002","unstructured":"Palsberg J, Ma D. A typed interrupt calculus. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. 2002, 291\u2013310"},{"key":"3251_CR10","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/3-540-44898-5_7","volume-title":"Proceedings of International Static Analysis Symposium","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: Proceedings of International Static Analysis Symposium. 2003, 109\u2013126"},{"key":"3251_CR11","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1109\/TSE.2004.64","volume":"30","author":"D Brylow","year":"2004","unstructured":"Brylow D, Palsberg J. Deadline analysis of interrupt-driven software. IEEE Transactions on Software Engineering, 2004, 30: 634\u2013655","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3251_CR12","first-page":"197","volume-title":"Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures","author":"B B\u00e9rard","year":"2009","unstructured":"B\u00e9rard B, Haddad S. Interrupt timed automata. In: Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures. 2009, 197\u2013211"},{"key":"3251_CR13","first-page":"69","volume-title":"Proceedings of the 17th International Symposium on Temporal Representation and Reasoning","author":"B B\u00e9rard","year":"2010","unstructured":"B\u00e9rard B, Haddad S, Sassolas M. Real time properties for interrupt timed automata. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning. 2010, 69\u201376"},{"key":"3251_CR14","first-page":"41","volume-title":"Proceedings of Formal Methods in System Design","author":"B B\u00e9rard","year":"2012","unstructured":"B\u00e9rard B, Haddad S, Sassolas M. Interrupt timed automata: verification and expressiveness. In: Proceedings of Formal Methods in System Design. 2012, 41\u201387"},{"key":"3251_CR15","first-page":"21","volume-title":"Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"G Li","year":"2009","unstructured":"Li G, Yuen S, Adachi M. Environmental simulation of real-time systems with nested interrupts. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 21\u201328."},{"key":"3251_CR16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/FI-1986-9202","volume":"9","author":"J C M Baeten","year":"1986","unstructured":"Baeten J C M, Bergstra J A, Klop J W. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Information IX(2), 1986, 9: 127\u2013168","journal-title":"Fundamenta Information IX(2)"},{"key":"3251_CR17","first-page":"5","volume-title":"Report P9417, Programming Research Group - University of Amsterdam","author":"B Diertens","year":"1994","unstructured":"Diertens B. New Features in PSF I - Interrupts, Disrupts, and Priorities. Report P9417, Programming Research Group - University of Amsterdam. 1994, 5\u201317"},{"key":"3251_CR18","first-page":"1","volume-title":"Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC","author":"A Engels","year":"1998","unstructured":"Engels A, Cobben T. Interrupt and disrupt in MSC: possibilities and problems. In: Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC. 1998, 1\u20134"},{"key":"3251_CR19","volume-title":"Prentice Hall","author":"C A R Hoare","year":"1985","unstructured":"Hoare C A R. Communicating Sequential Processes. Prentice Hall, 1985"},{"key":"3251_CR20","volume-title":"Prentice Hall","author":"C A R Hoare","year":"1998","unstructured":"Hoare C A R, He J. Unifying Theories of Programming. Prentice Hall, 1998"},{"key":"3251_CR21","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"C A R Hoare","year":"1993","unstructured":"Hoare C A R, He J. From algebra to operational semantics. Information Process Letter, 1993, 45: 75\u201380","journal-title":"Information Process Letter"},{"key":"3251_CR22","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S Brookes","year":"1996","unstructured":"Brookes S. Full abstraction for a shared-variable parallel language. Information and Computation, 1996, 127: 145\u2013163","journal-title":"Information and Computation"},{"key":"3251_CR23","volume-title":"The MIT Press","author":"J Bakker","year":"1996","unstructured":"Bakker J, Vink E. Control flow semantics. The MIT Press, 1996"},{"key":"3251_CR24","volume-title":"The Netherlands","author":"J Hartog","year":"2002","unstructured":"Hartog J. Probabilistic extensions of semantic models. Dissertation for PhD Degree, Vrije University, The Netherlands, 2002"},{"key":"3251_CR25","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1016\/S1571-0661(05)82521-6","volume":"22","author":"J Hartog","year":"1999","unstructured":"Hartog J, Vink E. Mixing up nondeterminism and probability: a preliminary report. Electrontic Notes Theoretical Computer Science, 1999, 22: 88\u2013110","journal-title":"Electrontic Notes Theoretical Computer Science"},{"key":"3251_CR26","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S1571-0661(05)80038-6","volume":"40","author":"J Hartog","year":"2001","unstructured":"Hartog J, Vink E, Bakker J. Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic Notes in Theoretical Computer Science, 2001, 40: 72\u201399","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3251_CR27","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1142\/S012905410200114X","volume":"13","author":"J Hartog","year":"2002","unstructured":"Hartog J, Vink E. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science, 2002, 13: 315\u2013340","journal-title":"International Journal of Foundations of Computer Science"},{"key":"3251_CR28","first-page":"449","volume-title":"Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods","author":"H Zhu","year":"2001","unstructured":"Zhu H, Bowen J P, He J. From operational semantics to denotational semantics for Verilog. In: Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. 2001, 449\u2013464"},{"key":"3251_CR29","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s11334-010-0134-z","volume":"6","author":"H Zhu","year":"2010","unstructured":"Zhu H, He J, Li J, Pu G, Bowen J P. Linking denotational semantics with operational semantics for web services. Innvoations Systems and Software Engineering, 2010, 6: 283\u2013298","journal-title":"Innvoations Systems and Software Engineering"},{"key":"3251_CR30","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.jlap.2011.06.003","volume":"81","author":"H Zhu","year":"2012","unstructured":"Zhu H, Yang F, He J, Bowen J P, Sanders J W, Qin S. Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. The Journal of Logic and Algebraic Programming, 2012, 81: 2\u201325","journal-title":"The Journal of Logic and Algebraic Programming"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-015-3251-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-015-3251-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-015-3251-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T07:06:50Z","timestamp":1651129610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-015-3251-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,3]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["3251"],"URL":"https:\/\/doi.org\/10.1007\/s11704-015-3251-x","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,3]]}}}