{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:41:19Z","timestamp":1777347679854,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540410553","type":"print"},{"value":"9783540453529","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45352-0_4","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T12:26:02Z","timestamp":1194956762000},"page":"19-30","source":"Crossref","is-referenced-by-count":32,"title":["Scaling up Uppaal"],"prefix":"10.1007","author":[{"given":"Henrik","family":"Ejersbo Jensen","sequence":"first","affiliation":[]},{"given":"Kim","family":"Guldstrand Larsen","sequence":"additional","affiliation":[]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"4_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Proc. 4th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998)","author":"L. Aceto","year":"1998","unstructured":"Luca Aceto, Augusto Burgueno, and Kim G. Larsen. Model checking via reachability testing for timed automata. In Bernhard Steffen, editor, Proc. 4th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998), volume 1384 of Lecture Notes in Computer Science, pages 263\u2013280. Springer, 1998."},{"key":"4_CR2","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":"4_CR3","unstructured":"R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP\u201990, volume 443, 1990."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013236, 1994.","journal-title":"Theoretical Computer Science"},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Mocha Modularity in Model Checking","author":"R. Alur","year":"1998","unstructured":"R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha Modularity in Model Checking. In Computer Aided Verification, Proc. 10th Int. Conference, volume 1427 of Lecture Notes in Computer Science, pages 521\u2013525. Springer Verlag, 1998."},{"key":"4_CR6","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, pages 22:181\u2013201, 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Verification of an Audio Protocol with Bus Collision Using Uppaal","author":"J. Bengtsson","year":"1996","unstructured":"Johan Bengtsson, David Griffioen, K\u00e5re Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Proceedings of CAV\u201996, volume 1102 of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"key":"4_CR8","unstructured":"D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, 1996."},{"key":"4_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0032342","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. Spinger Verlag, 1996."},{"key":"4_CR10","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":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49213-5_1","volume-title":"Compositionality: The Significant Difference, International Symposium, COMPOS\u201997","author":"W.-P. Roever de","year":"1998","unstructured":"Willem-Paul de Roever. The need for compositional proof systems: A survey. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Compositionality: The Significant Difference, International Symposium, COMPOS\u201997, volume 1536 of Lecture Notes in Computer Science, pages 1\u201322. Springer-Verlag, 1997."},{"key":"4_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-48778-6_17","volume-title":"Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS\u201999","author":"K. Havelund","year":"1999","unstructured":"K. Havelund, K. Larsen, and A. Skou. Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. In Joost-Pieter Katoen, editor, Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS\u201999, volume 1601 of Lecture Notes in Computer Science, pages 277\u2013298. Springer Verlag, 1999."},{"key":"4_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Automated Analysis of an Audio Control Protocol","author":"P.-H. Ho","year":"1995","unstructured":"Pei-Hsin Ho and Howard 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":"4_CR14","unstructured":"Henrik Ejersbo Jensen. Abstraction-Based Verification of Distributed Systems. PhD thesis, Aalborg University, Institute for Computer Science, Aalborg, Denmark, 1999."},{"key":"4_CR15","unstructured":"Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol Using SPIN and UPAAL. In J-C. Gregoire, G.J. Holzmann, and D.A. Peled, editors, Proceedings Second Workshop on the SPIN Verification System, American Mathematical Society, DIMACS\/39, 1996."},{"key":"4_CR16","unstructured":"K\u00e5re Jelling Kristoffersen. Compositional Verification of Concurrent Systems. PhD thesis, Aalborg University, Department of Computer Science, Institute for Electronic Systems, Aalborg, Denmark, August 1998."},{"key":"4_CR17","unstructured":"K.G. Larsen. Context-Dependent Bisimulation Between Processes. PhD thesis, University of Edinburgh, Mayfield Road, Edinburgh, Scotland, 1986."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"K.G. Larsen. A context dependent bisimulation between processes. Theoretical Computer Science, 49, 1987.","DOI":"10.1016\/0304-3975(87)90007-7"},{"issue":"1-2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134\u2013152, October 1997.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design, pages 6:11\u201344, 1995.","journal-title":"Formal Methods in System Design"},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Verification of an Implementation of Tomasulo\u2019s Algorithm by Compositional Model Checking","author":"K. L. McMillan","year":"1998","unstructured":"K. L. McMillan. Verification of an Implementation of Tomasulo\u2019s Algorithm by Compositional Model Checking. In Computer Aided Verification, Proc. 10th Int. Conference, volume 1427 of Lecture Notes in Computer Science, pages 110\u2013121. Springer Verlag, 1998."}],"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-45352-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T06:12:23Z","timestamp":1556950343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45352-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410553","9783540453529"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45352-0_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}