{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:19Z","timestamp":1725663859275},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540539810"},{"type":"electronic","value":"9783540464990"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3540539816_71","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:19:22Z","timestamp":1330208362000},"page":"259-282","source":"Crossref","is-referenced-by-count":5,"title":["Using higher order logic for modelling real-time protocols"],"prefix":"10.1007","author":[{"given":"Rachel","family":"Cardell-Oliver","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,7,6]]},"reference":[{"key":"17_CR1","volume-title":"Data Networks","author":"D. Bertsekas","year":"1987","unstructured":"Dimitri Bertsekas and Robert Gallagher. Data Networks. Prentice-Hall International, Englewood Cliffs, NJ, 1987."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.","DOI":"10.2307\/2266170"},{"key":"17_CR3","unstructured":"Rachel Cardell-Oliver. Formal verification of real-time protocols using higher order logic. Technical Report 206, University of Cambridge Computer Laboratory, August 1990."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, A.J.R.G. Milner, and C.P. Wadsworth. Edinburgh LCF: a mechanized logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"17_CR5","unstructured":"M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, pages 153\u2013177. North Holland, 1986."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Mike Gordon. A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis, Proceedings of the Workshop on Hardware Verification, Calgary, 12\u201316 January, 1987, G.M. Birtwistle and P.A. Subrahmanyam, eds. Kluwer International Series in Engineering and Computer Science, SECS35, pages 73\u2013128. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Roger Hale. Using temporal logic for prototyping: the design of a lift controller. In Temporal Logic in Specification 1987, pages 375\u2013408, 1987. Lecture Notes in Computer Science 398.","DOI":"10.1007\/3-540-51803-7_35"},{"issue":"5","key":"17_CR8","first-page":"242","volume":"133","author":"F.K. Hanna","year":"1986","unstructured":"F.K. Hanna and N. Daeche. Specification and verification of digital systems using higher-order predicate logic. IEE Proceedings E, 133 Part E(5):242\u2013254, September 1986.","journal-title":"IEE Proceedings E"},{"issue":"9","key":"17_CR9","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"SE-12","author":"F. Jahanian","year":"1986","unstructured":"Farnam Jahanian and Aloysius Ka-Lau Mok. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, SE-12(9):890\u2013904, September 1986.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR10","unstructured":"Jeffrey J. Joyce. Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Computer Laboratory, University of Cambridge, December 1989. also published as Computer Laboratory Technical Report 195."},{"key":"17_CR11","unstructured":"Thomas F. Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, Computer Laboratory, University of Cambridge, August 1989. also published as Computer Laboratory Technical Report 201."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Ben Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986.","DOI":"10.1007\/3-540-15670-4_6"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"P.M. Melliar-Smith. Extending interval logic to real time systems. In Temporal Logic in Specification 1987, pages 224\u2013242, 1987. Lecture Notes in Computer Science 398.","DOI":"10.1007\/3-540-51803-7_29"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Glenn H. MacEwen and David B. Skillicorn. Using Higher Order Logic for Modular Specification of Real-Time Distributed Systems, pages 37\u201366. Springer Verlag, September 1988. Lecture Notes in Computer Science 331.","DOI":"10.1007\/3-540-50302-1_2"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Faran Moller and Chris Tofts. A Temporal Calculus of Communicating Systems, pages 401\u2013415. Springer Verlag, August 1990. Lecture Notes in Computer Science 458.","DOI":"10.1007\/BFb0039073"},{"issue":"3","key":"17_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/65000.65003","volume":"7","author":"A. U. Shankar","year":"1989","unstructured":"A. Udaya Shankar. Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, 7(3):281\u2013316, August 1989.","journal-title":"ACM Transactions on Computer Systems"},{"issue":"2","key":"17_CR17","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF01667079","volume":"2","author":"A. U. Shankar","year":"1987","unstructured":"A. Udaya Shankar and Simon S. Lam. Time-dependent distributed systems: proving safety, liveness and real-time properties. Distributed Computing, 2(2):61\u201379, August 1987.","journal-title":"Distributed Computing"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '91"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3540539816_71.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:51:40Z","timestamp":1605646300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3540539816_71"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540539810","9783540464990"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3540539816_71","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}