{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:31Z","timestamp":1761597331235},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584681"},{"type":"electronic","value":"9783540489849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58468-4_165","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:16:10Z","timestamp":1330272970000},"page":"170-192","source":"Crossref","is-referenced-by-count":39,"title":["Verification of an audio control protocol"],"prefix":"10.1007","author":[{"given":"Doeko","family":"Bosscher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Indra","family":"Polak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"9_CR1","first-page":"1","volume-title":"volume 600 of Lecture Notes in Computer Science","author":"M. Abadi","year":"1992","unstructured":"M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de Bakker et al. [6], pages 1\u201327."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In Grossman et al. [10], pages 209\u2013229.","DOI":"10.1007\/3-540-57318-6_30"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and D.L. Dill. Automata for modeling real-time systems. In M. Paterson, editor, Proceedings 17 th ICALP, Warwick, volume 443 of Lecture Notes in Computer Science, pages 322\u2013335. Springer-Verlag, July 1990.","DOI":"10.1007\/BFb0032042"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14 th Annual IEEE Real-time Systems Symposium, 1993.","DOI":"10.1109\/REAL.1993.393520"},{"key":"9_CR5","volume-title":"Report CS-R94XX","author":"D.J.B. Bosscher","year":"1994","unstructured":"D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an audio control protocol. Report CS-R94XX, CWI, Amsterdam, 1994. To appear."},{"key":"9_CR6","volume-title":"volume 600 of Lecture Notes in Computer Science","author":"J.W. Bakker de","year":"1992","unstructured":"J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors. Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1992."},{"key":"9_CR7","volume-title":"The Coq proof assistant user's guide. Version 5.8. Technical report","author":"G. Dowek","year":"1993","unstructured":"G. Dowek, A. Felty, H. Herbelin, G.P. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA \u2014 Rocquencourt, May 1993."},{"key":"9_CR8","volume-title":"Technical Report MIT\/LCS\/TR-587","author":"R. Gawlick","year":"1993","unstructured":"R. Gawlick, R. Segala, J. S\u00d8gaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. Technical Report MIT\/LCS\/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993. An extended abstract will appear in Proceedings ICALP'94."},{"key":"9_CR9","unstructured":"W.O.D. Griffioen. Analysis of an Audio Control Protocol wi th Bus Collision. Master thesis, Programming Research Group, University of Amsterdam, 1994."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6"},{"key":"9_CR11","series-title":"Number 806 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Proceedings International Workshop TYPES'93","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, editors, Proceedings International Workshop TYPES'93, Nijmegen, The Netherlands, May 1993, number 806 in Lecture Notes in Computer Science, pages 127\u2013165. Springer-Verlag, 1994. Full version available as Report CS-R9420, CWI, Amsterdam, March 1994."},{"key":"9_CR12","volume-title":"Report CS-R9366","author":"A.S.A. Jeffrey","year":"1993","unstructured":"A.S.A. Jeffrey, S.A. Schneider, and F.W. Vaandrager. A comparison of additivity axioms in timed transition systems. Report CS-R9366, CWI, Amsterdam, November 1993."},{"key":"9_CR13","unstructured":"L. Lamport. A temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"L. Lamport. Hybrid systems in TLA+. In Grossman et al. [10], pages 77\u2013102.","DOI":"10.1007\/3-540-57318-6_25"},{"key":"9_CR15","unstructured":"B.W. Lampson, N.A. Lynch, and J.F. S\u00d8gaard-Andersen. Correctness of at-most-once message delivery protocols. In Formal Description Techniques VI. North-Holland, 1993."},{"key":"9_CR16","unstructured":"N.A. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing, pages 137\u2013151, August 1987. A full version is available as MIT Technical Report MIT\/LCS\/TR-387.","DOI":"10.1145\/41840.41852"},{"key":"9_CR18","volume-title":"Report CS-R9313","author":"N.A. Lynch","year":"1993","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations \u2014 part I: Untimed systems. Report CS-R9313, CWI, Amsterdam, March 1993."},{"key":"9_CR19","volume-title":"Report CS-R9314","author":"N.A. Lynch","year":"1993","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations \u2014 part II: Timing-based systems. Report CS-R9314, CWI, Amsterdam, March 1993."},{"key":"9_CR20","first-page":"447","volume-title":"volume 600 of Lecture Notes in Computer Science","author":"O. Maler","year":"1992","unstructured":"O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In de Bakker et al. [6], pages 447\u2013484."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Verifying hybrid systems. In Grossman et al. [10], pages 4\u201335.","DOI":"10.1007\/3-540-57318-6_22"},{"issue":"1","key":"9_CR22","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/BF01211081","volume":"6","author":"J.S. Moore","year":"1994","unstructured":"J.S. Moore. A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Journal of Formal Aspects of Computing Science, 6(1):60\u201391, 1994.","journal-title":"Journal of Formal Aspects of Computing Science"},{"key":"9_CR23","first-page":"376","volume-title":"volume 575 of Lecture Notes in Computer Science","author":"X. Nicollin","year":"1992","unstructured":"X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In K.G. Larsen and A. Skou, editors, Proceedings of the 3rd International Workshop on Computer Aided Verification, Aalborg, Denmark, volume 575 of Lecture Notes in Computer Science, pages 376\u2013398. Springer-Verlag, 1992."},{"issue":"4","key":"9_CR24","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319\u2013340, 1976.","journal-title":"Acta Informatica"},{"issue":"1","key":"9_CR25","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/32.210306","volume":"19","author":"A.P. Ravn","year":"1993","unstructured":"A.P. Ravn, H. Rischel, and K.M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41\u201355, January 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR26","unstructured":"R.S. Roden. Digital Communication Systems Design. Prentice Hall, 1988."},{"key":"9_CR27","series-title":"Volume 630 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/BFb0084808","volume-title":"Proceedings CONCUR 92","author":"F.W. Vaandrager","year":"1992","unstructured":"F.W. Vaandrager and N.A. Lynch. Action transducers and timed automata. In W.R. Cleaveland, editor, Proceedings CONCUR 92, Stony Brook, NY, USA, volume 630 of Lecture Notes in Computer Science, pages 436\u2013455. Springer-Verlag, 1992."},{"key":"9_CR28","series-title":"Volume 458 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/BFb0039080","volume-title":"Proceedings CONCUR 90","author":"Y. Wang","year":"1990","unstructured":"Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 502\u2013520. Springer-Verlag, 1990."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58468-4_165.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:21:43Z","timestamp":1605648103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58468-4_165"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584681","9783540489849"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-58468-4_165","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}