{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:39:19Z","timestamp":1761590359435,"version":"build-2065373602"},"reference-count":24,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4034,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1016\/s1567-8326(02)00036-x","type":"journal-article","created":{"date-parts":[[2002,10,8]],"date-time":"2002-10-08T16:46:42Z","timestamp":1034095602000},"page":"163-181","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":27,"special_numbering":"C","title":["Automated verification of an audio-control protocol using Uppaal"],"prefix":"10.1016","volume":"52-53","author":[{"given":"Johan","family":"Bengtsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.O.","family":"David 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":"78","reference":[{"key":"10.1016\/S1567-8326(02)00036-X_BIB1","series-title":"Modelling and Verification of Parallel Processes, Lecture Notes in Computer Science, vol. 2067","first-page":"100","article-title":"Uppaal\u2014Now, next, and future","author":"Amnell","year":"2001"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB2","series-title":"in: Proceedings of the International Colloquium on Algorithms Languages and Programming, Lecture Notes in Computer Science, vol. 443","first-page":"322","article-title":"Automata for modelling real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB3","series-title":"Proceedings of Workshop on Verification and Control of Hybrid Systems III, Lecture Notes in Computer Science, vol. 1066","first-page":"220","article-title":"Timing analysis in COSPAN","author":"Alur","year":"1995"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB4","series-title":"in: Proceedings of the 8th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1102","first-page":"244","article-title":"Verification of an audio protocol with bus collision using Uppaal","author":"Bengtsson","year":"1996"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB5","doi-asserted-by":"crossref","unstructured":"J. Bengtsson, F. Larsson, Uppaal a tool for automatic verification of real-time systems, Master\u2019s thesis, Uppsala University, 1996. Available from http:\/\/www.docs.uu.se\/docs\/rtmv\/bl-report.pdf","DOI":"10.7146\/brics.v3i58.18769"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB6","series-title":"in: Proceedings of Workshop on Verification and Control of Hybrid Systems III, Lecture Notes in Computer Science, vol. 1066","first-page":"232","article-title":"Uppaal\u2014a tool suite for automatic verification of real\u2013time systems","author":"Bengtsson","year":"1995"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB7","unstructured":"J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, C. Weise, New Generation of Uppaal, in: International Workshop on Software Tools for Technology Transfer, June 1998"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB8","doi-asserted-by":"crossref","unstructured":"D. Bosscher, I. Polak, F. Vaandrager, Verification of an audio-control protocol, in: Proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, vol. 863, 1994","DOI":"10.1007\/3-540-58468-4_165"},{"issue":"4","key":"10.1016\/S1567-8326(02)00036-X_BIB9","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: state of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB10","series-title":"in: Proceedings of the 16th IEEE Real-Time Systems Symposium","first-page":"66","article-title":"Two examples of verification of multirate timed automata with Kronos","author":"Daws","year":"1995"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB11","unstructured":"W.O. David Griffioen. Analysis of an Audio Control Protocol with Bus Collision, Master\u2019s thesis, University of Amsterdam, Programming Research Group, 1994"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB12","series-title":"in: Proceedings of the 16th IEEE Real-Time Systems Symposium","first-page":"56","article-title":"HyTech: the next generation","author":"Henzinger","year":"1995"},{"issue":"1-2","key":"10.1016\/S1567-8326(02)00036-X_BIB13","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050008","article-title":"HyTech: a model checker for hybrid systems","volume":"1","author":"Henzinger","year":"1997","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"10.1016\/S1567-8326(02)00036-X_BIB14","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Information and Computation"},{"year":"1991","series-title":"The Design and Validation of Computer Protocols","author":"Holzmann","key":"10.1016\/S1567-8326(02)00036-X_BIB15"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB16","series-title":"in: Proceedings of the 7th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 939","article-title":"Automated analysis of an audio control protocol","author":"Ho","year":"1995"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB17","series-title":"in: Proceedings of the 18th IEEE Real-Time Systems Symposium","first-page":"14","article-title":"Efficient verification of real-time systems: compact data structures and state-space reduction","author":"Larsson","year":"1997"},{"issue":"1\u20132","key":"10.1016\/S1567-8326(02)00036-X_BIB18","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB19","series-title":"Proceedings of the 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1254","first-page":"456","article-title":"Uppaal: status and developments","author":"Larsen","year":"1997"},{"issue":"1\u20132","key":"10.1016\/S1567-8326(02)00036-X_BIB20","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/s100090050006","article-title":"Continuous modeling of real-time and hybrid systems: from concepts to tools","volume":"1","author":"Larsen","year":"1997","journal-title":"International Journal on Software Tools for Technology Transfer"},{"year":"1989","series-title":"Communication and Concurrency","author":"Milner","key":"10.1016\/S1567-8326(02)00036-X_BIB21"},{"issue":"1","key":"10.1016\/S1567-8326(02)00036-X_BIB22","first-page":"88","article-title":"Parametric real-time model checking using splitting trees","volume":"8","author":"LutjeSpelberg","year":"2001","journal-title":"Nordic Journal"},{"issue":"1\u20132","key":"10.1016\/S1567-8326(02)00036-X_BIB23","first-page":"134","article-title":"A verification tool for real time systems","volume":"1","author":"Yovine","year":"1997","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1567-8326(02)00036-X_BIB24","series-title":"Proceedings of the 7th International Conference on Formal Description Techniques","first-page":"223","article-title":"Automatic verification of real-time communicating systems by constraint-solving","author":"Yi","year":"1994"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260200036X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S156783260200036X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:35:16Z","timestamp":1761590116000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S156783260200036X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":24,"alternative-id":["S156783260200036X"],"URL":"https:\/\/doi.org\/10.1016\/s1567-8326(02)00036-x","relation":{},"ISSN":["1567-8326"],"issn-type":[{"type":"print","value":"1567-8326"}],"subject":[],"published":{"date-parts":[[2002,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Automated verification of an audio-control protocol using Uppaal","name":"articletitle","label":"Article Title"},{"value":"The Journal of Logic and Algebraic Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1567-8326(02)00036-X","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier Inc.","name":"copyright","label":"Copyright"}]}}