{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T04:15:56Z","timestamp":1771042556468,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:41:12Z","timestamp":1330292472000},"page":"244-256","source":"Crossref","is-referenced-by-count":50,"title":["Verification of an Audio Protocol with bus collision using Uppaal"],"prefix":"10.1007","author":[{"given":"Johan","family":"Bengtsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W. O. David","family":"Griffioen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K\u00e5re J.","family":"Kristoffersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fredrik","family":"Larsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"21_CR1","unstructured":"R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP'90, LNCS 443, 1990."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Johan Bengtsson and Fredrik Larsson. Uppaal a Tool for Automatic Verification of Real-time Systems, Master's thesis, Uppsala University, 1996.","DOI":"10.1007\/BFb0020949"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal \u2014 a Tool Suite for Automatic Verification of Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995. To appear in LNCS, 1996.","DOI":"10.1007\/BFb0020949"},{"key":"21_CR4","first-page":"170","volume":"863","author":"D.J.B. Bosscher","year":"1994","unstructured":"D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an Audio-Control Protocol. In Proc. of FTRTFT'94, LNCS 863, pages 170\u2013192, 1994.","journal-title":"LNCS"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 66\u201375, December 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"21_CR6","unstructured":"W.O.D. Griffioen. Analysis of an Audio Control Protocol with Bus Collision. Master's thesis, University of Amsterdam, Programming Research Group, 1994."},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: The Next Generation. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 56\u201365, December 1995.","DOI":"10.1109\/REAL.1995.495196"},{"key":"21_CR8","first-page":"223","volume":"864","author":"N. Halbwachs","year":"1994","unstructured":"N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximations. In Static Analysis Symposium, LNCS 864, pages 223\u2013237, 1994.","journal-title":"LNCS"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Pei-Hsin Ho and Howard Wong-Toi. Automated Analysis of an Audio Control Protocol. In Proc. of CAV'95, LNCS 939, 1995.","DOI":"10.1007\/3-540-60045-0_64"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995. To appear in LNCS, 1996.","DOI":"10.7146\/brics.v3i57.18682"},{"key":"21_CR11","unstructured":"Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:19:13Z","timestamp":1742599153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}