{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:13:40Z","timestamp":1725747220187},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397172"},{"type":"electronic","value":"9783642397189"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39718-9_22","type":"book-chapter","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T03:01:54Z","timestamp":1377831714000},"page":"373-390","source":"Crossref","is-referenced-by-count":2,"title":["Reactive Designs of Interrupts in Circus Time"],"prefix":"10.1007","author":[{"given":"Kun","family":"Wei","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: essays in Honour of C.A.R. Hoare, ch. 21. Prentice-Hall (1994)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A.L.C. Cavalcanti","year":"2006","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol.\u00a03167, pp. 220\u2013268. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"22_CR3","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A.L.C. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing\u00a015(2-3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle\/Circus : A Process Specification and Verification Environment. Technical Report 1547, LRI, Universit\u00e9 Paris-Sud XI (November 2011), \n                  \n                    http:\/\/www.lri.fr\/Rapports-internes","DOI":"10.1007\/978-3-642-27705-4_20"},{"key":"22_CR5","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)"},{"key":"22_CR6","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall International (1998)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-33296-8_11","volume-title":"Formal Methods: Foundations and Applications","author":"Y. Huang","year":"2012","unstructured":"Huang, Y., Zhao, Y., Shi, J., Zhu, H., Qin, S.: Investigating time properties of interrupt-driven programs. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol.\u00a07498, pp. 131\u2013146. Springer, Heidelberg (2012)"},{"key":"22_CR8","unstructured":"Jifeng, H.: From CSP to hybrid systems, pp. 171\u2013189 (1994)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"22_CR10","unstructured":"McEwan, A., Woodcock, J.C.P.: Unifying theories of interrupts. In: Proceedings of the Second UTP Symposium, Trinity College Dublin (2008)"},{"key":"22_CR11","volume-title":"Programming from specifications","author":"C. Morgan","year":"1990","unstructured":"Morgan, C.: Programming from specifications. Prentice-Hall, Inc., Upper Saddle River (1990)"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Unifying theories in ProofPower-Z. Formal Aspects of Computing Journal (2007)","DOI":"10.1007\/s00165-007-0044-5"},{"key":"22_CR13","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International (1998)"},{"key":"22_CR14","unstructured":"Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons (1999)"},{"issue":"2","key":"22_CR15","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A. Sherif","year":"2010","unstructured":"Sherif, A., Cavalcanti, A.L.C., Jifeng, H., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing\u00a022(2), 153\u2013191 (2010)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Wei, K., Woodcock, J.C.P., Burns, A.: A timed model of Circus with the reactive design miracle. In: 8th International Conference on Software Engineering and Formal Methods (SEFM), Pisa, Italy, pp. 315\u2013319. IEEE Computer Society (September 2010)","DOI":"10.1109\/SEFM.2010.40"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Wei, K., Woodcock, J.C.P., Burns, A.: Timed Circus: Timed CSP with the Miracle. In: ICECCS, pp. 55\u201364 (2011)","DOI":"10.1109\/ICECCS.2011.13"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus Time with reactive designs. In: UTP, pp. 68\u201387 (2012)","DOI":"10.1007\/978-3-642-35705-3_3"},{"key":"22_CR19","unstructured":"Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: New Circus Time. Technical report, Department of Computer Science, University of York, UK (March 2012), \n                  \n                    http:\/\/www.cs.york.ac.uk\/circus\/hijac\/publication.html"},{"key":"22_CR20","volume-title":"Using Z: Specification, Refinement and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)"},{"key":"22_CR21","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: Butterfield, A., Pahl, C. (eds.) IWFM 2001:\u00a05th Irish Workshop in Formal Methods, BCS Electronic Workshops in Computing, Dublin, Ireland (July 2001)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.C.P. Woodcock","year":"2002","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of $ Circus$. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-24756-2_4","volume-title":"Integrated Formal Methods","author":"J.C.P. Woodcock","year":"2004","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 40\u201366. Springer, Heidelberg (2004)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Huang, Y., He, J., Liu, S.: Formal Model of Interrupt Program from a Probabilistic Perspective. In: ICECCS, pp. 87\u201394 (2011)","DOI":"10.1109\/ICECCS.2011.16"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2013"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39718-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:26:26Z","timestamp":1558052786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39718-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397172","9783642397189"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39718-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}