{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T16:58:58Z","timestamp":1780505938105,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540427872","type":"print"},{"value":"9783540455103","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45510-8_4","type":"book-chapter","created":{"date-parts":[[2007,11,6]],"date-time":"2007-11-06T02:12:16Z","timestamp":1194315136000},"page":"99-124","source":"Crossref","is-referenced-by-count":42,"title":["UPPAAL - Now, Next, and Future"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Amnell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerd","family":"Behrmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johan","family":"Bengtsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pedro R.","family":"D\u2019Argenio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"David","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ansgar","family":"Fehnker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Hune","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bertrand","family":"Jeannet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M. Oliver","family":"M\u00f6ller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carsten","family":"Weise","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,10,16]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Rajeev Alur, Costas Courcoubetis, and David Dill. Model Checking in Dense Real Time. Information and Computation, 104:2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David Dill, and Howard Wong-Toi. Minimization of Timed Transition Systems. In Proc. of CONCUR\u2019 92, Theories of Concurrency: Unification an d Extension, pages 340\u2013354, 1992.","DOI":"10.1007\/BFb0084802"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric Real-time Reasoning. In Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, pages 592\u2013601, 1993.","DOI":"10.1145\/167088.167242"},{"key":"4_CR4","unstructured":"Tobias Amnell and Pontus Jansson. Report from astec-rt auto project-central locking system case study. In preparation, 2001."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-48320-9_9","volume-title":"Proc. of CONCUR\u2019 99: Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Rajeev Alur and Bow-Yaw Wang. \u201cNext\u201d Heuristic for On-the-fly Model Checking. In Proc. of CONCUR\u2019 99: Concurrency Theory, number 1664 in Lecture Notes in Computer Science, pages 98\u2013113. Springer-Verlag, 1999."},{"key":"4_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Proc. of the 10th Int. Conf. on Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: A model-Checking Tool for Real-Time Systems. In Proc. of the 10th Int. Conf. on Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 546\u2013550. Springer-Verlag, 1998."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. Efficient Guiding Towards Cost-Optimality in uppaal. Accepted for publication in TACAS\u20192001.","DOI":"10.7146\/brics.v8i4.20458"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. Submitted for publication. Available at http:\/\/www.docs.uu.se\/docs\/rtmv\/papers\/-bfhlprv-sub00-1.ps.gz , 2000.","DOI":"10.7146\/brics.v8i3.20457"},{"key":"4_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Proc. of the 12th Int. Conf. on Computer Aided Verification","author":"]. G. Behrmann","year":"2000","unstructured":"]_ Gerd Behrmann, Thomas Hune, and Frits Vaandrager. Distributing Timed Model Checking-How the Search Order Matters. In Proc. of the 12th Int. Conf. on Computer Aided Verification, number 1855 in Lecture Notes in Computer Science, pages 216\u2013231. Springer-Verlag, 2000."},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055643","volume-title":"Proc. of CONCUR\u2019 98: Concurrency Theory","author":"J. Bengtsson","year":"1998","unstructured":"Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. Partial Order Reductions for Timed Systems. In Proc. of CONCUR\u2019 98: Concurrency Theory, number 1466 in Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Proc. of the 11th Int. Conf. on Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proc. of the 11th Int. Conf. on Computer Aided Verification, number 1633 in Lecture Notes in Computer Science. Springer-Verlag, 1999."},{"key":"4_CR12","unstructured":"Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, 1998."},{"issue":"8","key":"4_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Randal E. Bryant. Graph-Based Algorithms for Boolean-Function Manipulation. IEEE Trans. on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Giosu\u00e8 Bandini, R. F. Lutje Spelberg, R. C. M. de Rooij, and W. J. Toetenel. Application of Parametric Model Checking-The Root Contention Protocol. In Proc. of the 34th Annual Hawaii International Conference on System Sciences (HICSS-34), 2001.","DOI":"10.1109\/HICSS.2001.927265"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proc. of the 4th ACM Symposium on Principles of Programming Languages, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"Proc. of CONCUR\u2019 2000: Concurrency Theory","author":"F. Cassez","year":"2000","unstructured":"Franck Cassez and Kim G. Larsen. The Impressive Power of Stopwatches. In Proc. of CONCUR\u2019 2000: Concurrency Theory, number 1877 in Lecture Notes in Computer Science, pages 138\u2013152. Springer-Verlag, 2000."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Alexandre David and Wang Yi. Modelling and Analysis of a Commercial Field Bus Protocol. In Proc. of 12th Euromicro Conference on Real-Time Systems, pages 165\u2013172. IEEE Computer Society Press, June 2000.","DOI":"10.1109\/EMRTS.2000.854004"},{"key":"4_CR18","unstructured":"Christer Ericsson, Anders Wall, and Wang Yi. Timed Automata as Task Models for Eventdriven Systems. In Proceedings of RTSCA 99. IEEE Computer Society Press, 1999."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Ansgar Fehnker. Scheduling a Steel Plant with Timed Automata. In Proc. of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA99), pages 280\u2013286. IEEE Computer Society Press, 1999.","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"David Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proc. of the 9th Int. Conf. on Computer Aided Verification","author":"T. A. Henzinger","year":"1997","unstructured":"Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A Model Checker for Hybrid Systems. In Orna Grumberg, editor, Proc. of the 9th Int. Conf. on Computer Aided Verification, number 1254 in Lecture Notes in Computer Science, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. A","year":"1994","unstructured":"Hans A. Hansson and Bengt Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6:512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Thomas Hune, Kim G. Larsen, and Paul Pettersson. Guided Synthesis of Control Programs Using uppaal. In Ten H. Lai, editor, Proc. of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation, pages E15\u2013E22. IEEE Computer Society Press, April 2000.","DOI":"10.7146\/brics.v7i37.20203"},{"key":"4_CR24","unstructured":"Thomas Hune. Modelling a Real-time Language. In Proceedings of FMICS, 1999."},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Torsten K. Iversen, K\u00e5re J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, and Chris B. Thomasen. Model-Checking Real-Time Control Programs-Verifying LEGO Mindstorms Systems Using uppaal. In Proc. of 12th Euromicro Conference on Real-Time Systems, pages 147\u2013155. IEEE Computer Society Press, June 2000.","DOI":"10.1109\/EMRTS.2000.854002"},{"key":"4_CR26","unstructured":"Bertrand Jeannet. Dynamic Partitioning in Linear Relation Analysis. Application to the Verification of Reactive Systems. to appear in Formal Methods and System Design, Kluwer Academic Press."},{"key":"4_CR27","unstructured":"Bertrand Jeannet. Partitionnement dynamique dans l\u2019analyse de relations lin\u00e9aires et application \u00e0 la v\u00e9rification de programmes synchrones. PhD thesis, Institut National Polytechnique de Grenoble, September 2000."},{"key":"4_CR28","unstructured":"Henrik E. Jensen. Model Checking Probabilistic Real Time Systems. In B. Bjerner, M. Larsson, and B. Nordstr\u00f6m, editors, Proceedings of the 7th Nordic Workshop on Programming Theory, G\u00f6teborg Sweden, Report 86, pages 247\u2013261. Chalmers University of Technolog, 1996."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Bertrand Jeannet, Nicolas Halbwachs, and Pascal Raymond. Dynamic Partitioning in Analyses of Numerical Properties. In Static Analysis Symposium, SAS\u201999, Venezia (Italy), September 1999.","DOI":"10.1007\/3-540-48294-6_3"},{"key":"4_CR30","volume-title":"Vhs Case Study 1-experimental Batch Plant using uppaal","author":"K. Kristoffersen","year":"1999","unstructured":"K\u00e5re Kristoffersen, Kim G. Larsen, Paul Pettersson, and Carsten Weise. Vhs Case Study 1-experimental Batch Plant using uppaal. BRICS, University of Aalborg, Denmark, http:\/\/www.cs.auc.dk\/research\/-FS\/VHS\/cs1uppaal.ps.gz , May 1999."},{"key":"4_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-48778-6_5","volume-title":"Proceedings of the 5th AMAST Workshop on Real-Time and Probabilistic System","author":"M. Z. Kwiatkowska","year":"1999","unstructured":"Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic Verification of Real-Time Systems with Probability Distributions. In J.-P. Katoen, editor, Proceedings of the 5th AMAST Workshop on Real-Time and Probabilistic System, Bamberg, Germany, number 1601 in Lecture Notes in Computer Science, pages 75\u201395. Springer-Verlag, 1999. An extended version will appear in Theoretical Computer Science."},{"issue":"1","key":"4_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Leslie Lamport. A Fast Mutual Exclusion Algorithm. ACM Trans. on Computer Systems, 5(1):1\u201311, February 1987. Also appeared as SRC Research Report 7.","journal-title":"ACM Trans. on Computer Systems"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Kristina Lundqvist, Lars Asplund, and Stephen Michell. A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects. In Springer-Verlag, editor, Proc. of the Ada Europe Conference, pages 12\u201325, 1999.","DOI":"10.1007\/3-540-48753-0_2"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. Submitted for publication, 2001.","DOI":"10.1007\/3-540-44585-4_47"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Fredrik Larsson, Kim G. Larsen, Paul Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 14\u201324. IEEE Computer Society Press, December 1997.","DOI":"10.1109\/REAL.1997.641265"},{"key":"4_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0054173","volume-title":"Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Lind-Nielsen","year":"1998","unstructured":"J\u00f8rn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, K\u00e5re J. Kristoffersen, and Kim G. Larsen. Verification of Large State\/Event Systems Using Compositionality and Dependency Analysis. In Bernard Steffen, editor, Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 201\u2013216. Springer-Verlag, 1998."},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Henrik L\u00f6nn and Paul Pettersson. Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, pages 235\u2013242, December 1997.","DOI":"10.1109\/PRFTS.1997.640153"},{"issue":"1-2","key":"4_CR38","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"},{"issue":"3","key":"4_CR39","first-page":"271","volume":"6","author":"K. G. Larsen","year":"1999","unstructured":"Kim G. Larsen, Carsten Weise, Wang Yi, and Justin Pearson. Clock Difference Diagrams. Nordic Journal of Computing, 6(3):271\u2013298, 1999.","journal-title":"Nordic Journal of Computing"},{"key":"4_CR40","unstructured":"Antoine Min\u00e9. The Numerical Domain of Octagons and Application to the Automatic Analysis of Programs. Master\u2019s thesis, \u00c9cole Normale Sup\u00e9rieure de Paris, 2000."},{"key":"4_CR41","unstructured":"Paul Pettersson. Modelling and Analysis of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Department of Computer Systems, Uppsala University, February 1999."},{"key":"4_CR42","first-page":"331","volume":"30","author":"W. J. Paul","year":"1980","unstructured":"Wolfgang J. Paul and Janos Simon. Decision Trees and Random Access Machines. In Logic and Algorithmic, volume 30 of Monographie de L\u2019Enseignement Math\u00e9matique, pages 331\u2013340. L\u2019Enseignement Math\u00e9matique, Universit\u00e9 de Gen\u00e8ve, 1980.","journal-title":"Logic and Algorithmic"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Ulrich Stern and David L. Dill. Parallelizing the Mur\u00f8 Verifier. In Orna Grumberg, editor, Proc. of the 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 256\u2013267. Springer-Verlag, June 1997. Haifa, Isreal, June 22-25.","DOI":"10.1007\/3-540-63166-6_26"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Karsten Strehl and Lothar Thiele. Symbolic Model Checking of Process Networks Using Interval Diagram Techniques. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD-98), pages 686\u2013692, 1998.","DOI":"10.1145\/288548.289117"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Sergio Yovine. Kronos: A verification Tool for Real-Time Systems. Springer International Journal of Software Tools for Technology Transfer, 1(1\/2), October 1997.","DOI":"10.1007\/s100090050009"},{"key":"4_CR46","unstructured":"Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Dieter Hogrefe and Stefan Leue, editors, Proc. of the 7th Int. Conf. on Formal Description Techniques, pages 223\u2013238. North-Holland, 1994."}],"container-title":["Lecture Notes in Computer Science","Modeling and Verification of Parallel Processes"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45510-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T05:49:47Z","timestamp":1556948987000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45510-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427872","9783540455103"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/3-540-45510-8_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}