{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:10:23Z","timestamp":1761487823284},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_17","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"277-298","source":"Crossref","is-referenced-by-count":22,"title":["Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"17_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Proceedings of TACAS\u201998","author":"L. Aceto","year":"1998","unstructured":"L. Aceto, A. Bergueno, and K. G. Larsen. Model Checking via Reachability Testing for Timed Automata. In B. Steffen, editor, Proceedings of TACAS\u201998, volume 1384 of Lecture Notes in Computer Science, pages 263\u2013280, 1998."},{"key":"17_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of FST TCS\u201998","author":"L. Aceto","year":"1998","unstructured":"L. Aceto, P. Bouyer, A. Burgueno, and K. G. Larsen. The Limit of Testing for Timed Automata. In Proceedings of FST TCS\u201998, Lecture Notes in Computer Science, 1998."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proc. of Logic in Computer Science, pages 414\u2013425. IEEE Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of ICALP\u201990","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP\u201990, volume 443 of Lecture Notes in Computer Science, 1990."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV\u201996","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, D. Griffioen, K. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Proc. of CAV\u201996, volume 1102 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Bengtsson","year":"1995","unstructured":"J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal \u2014 A Tool Suite for Symbolic and Compositional Verification of Real-Time Systems. In Proc. of the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science. Springer-Verlag, May 1995."},{"key":"17_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-61042-1_66","volume-title":"Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal in 1995. In Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in Lecture Notes in Computer Science, pages 431\u2013434. Springer-Verlag, March 1996."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"A. Bouali, A. Ressouche, and V. Roy R. de Simone. The FC2Toolset. Lecture Notes in Computer Science, 1102, 1996.","DOI":"10.1007\/BFb0014350"},{"key":"17_CR9","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. Modelling and Verifying a Bounded Retransmission Protocol. In Proc. of COST 247, International Workshop on Applied Formal Methods in System Design, 1996."},{"key":"17_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III, Verification and Control","author":"C. Daws","year":"1996","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, volume 1066 of Lecture Notes in Computer Science, pages 208\u2013219. Springer-Verlag, 1996."},{"key":"17_CR11","unstructured":"C. Ericsson, A. Wall, and W. Yi. Timed Automata as Task Models for Event-Driven Systems. In Proceedings of Nordic Workshop on Programming Theory, 1998. To appear in a special issue of Nordic Journal of Computing."},{"key":"17_CR12","unstructured":"K. Havelund, K. G. Larsen, and A. Skou. Documentation of the Modeling and Verification of Bang & Olufsens\u2019s IOP Power Down Module in Uppaal. Internal AUC document delivered to B&O. Early version of this report., September 1997."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"K. Havelund, A. Skou, K. G. Larsen, and K. Lund. Formal Modeling and Analysis of an Audio\/Video Protocol: An Industrial Case Study Using Uppaal. In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 2\u201313, Dec 1997. San Francisco, California, USA.","DOI":"10.1109\/REAL.1997.641264"},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV\u201995","author":"P.-H. Ho","year":"1995","unstructured":"P.-H. Ho and H. Wong-Toi. Automated Analysis of an Audio Control Protocol. In Proc. of CAV\u201995, volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995."},{"key":"17_CR15","unstructured":"G. Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"H.E. Jensen, K.G. Larsen, and A. Skou. Modelling and Analysis of a Collision Avoidance Protocol Using SPIN and UPPAAL. In The Second Workshop on the SPIN Verification System, volume 32 of DIMACS, Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1996.","DOI":"10.7146\/brics.v3i24.20005"},{"key":"17_CR17","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Diagnostic Model Checking for Real-Time Systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"M. Lindahl, P. Pettersson, and W. Yi. Formal Design and Analysis of a Gear-Box Controller. In Bernhard Steffen, editor, Proc. of the 4th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems \u2014 LNCS 1384, pages 281\u2013297. Gulbelkian Foundation, March 1998. Lisbon, Portugal.","DOI":"10.1007\/BFb0054178"},{"key":"17_CR19","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989."},{"key":"17_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TACAS\u201999","author":"S. Tripakis","year":"1999","unstructured":"S. Tripakis. Timed Diagnostics for Reachability Properties. In Proceedings of TACAS\u201999, Lecture Notes in Computer Science, 1999."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T16:34:53Z","timestamp":1556382893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}