{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T09:50:20Z","timestamp":1693043420365},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540441656","type":"print"},{"value":"9783540457398","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45739-9_1","type":"book-chapter","created":{"date-parts":[[2007,5,16]],"date-time":"2007-05-16T02:42:01Z","timestamp":1179283321000},"page":"3-22","source":"Crossref","is-referenced-by-count":66,"title":["UppaaL Implementation Secrets"],"prefix":"10.1007","author":[{"given":"Gerd","family":"Behrmann","sequence":"first","affiliation":[]},{"given":"Johan","family":"Bengtsson","sequence":"additional","affiliation":[]},{"given":"Alexandre","family":"David","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,4]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-45510-8_4","volume-title":"Modelling and Verification of Parallel Processes","author":"T. Amnell","year":"2001","unstructured":"Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D\u2019Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver M\u00f6ller, Paul Pettersson, Carsten Weise, and Wang Yi. Uppaal-Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verification of Parallel Processes, number 2067 in Lecture Notes in Computer Science, pages 100\u2013125. Springer-Verlag, 2001."},{"key":"1_CR2","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":"1_CR3","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":"1_CR4","unstructured":"Gerd Behrmann. A performance study of distributed timed automata reachability analysis. Submitted."},{"key":"1_CR5","unstructured":"Richard Bellman. Dynamic Programming. Princeton University Press, 1957."},{"key":"1_CR6","unstructured":"Johan Bengtsson. Clocks, DBMs and STates in Timed Systems. PhD thesis, Faculty of Science and Technology, Uppsala University, 2002."},{"key":"1_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of TACAS\u20192001","author":"G. Behrmann","year":"2001","unstructured":"Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim Larsen, Paul Petterson, and Judi Romijn. Efficient guiding towards cost-optimality in uppaal. In Proc. of TACAS\u20192001, Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"key":"1_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61474-5_73","volume-title":"Proc. of the 8th Int. Conf. on Computer Aided Verification","author":"J. Bengtsson","year":"1996","unstructured":"Johan Bengtsson, W.O. David Griffioen, K\u00e5re J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of the 8th Int. Conf. on Computer Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 244\u2013256. Springer-Verlag, July 1996."},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 12th International Conference on Computer Aided Verification","author":"G. Behrmann","year":"2000","unstructured":"Gerd Behrmann, Thomas Hune, and Frits Vaandrager. Distributed timed model checking-How the search order matters. In Proc. of 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Chicago, Juli 2000. Springer-Verlag."},{"key":"1_CR10","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":"Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang 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":"1_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":"1_CR12","doi-asserted-by":"crossref","unstructured":"Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"1_CR14","unstructured":"Alexandre David, Gerd Behrmann, Kim G. Larsen, and Wang Yi. The next generation of uppaal. Submitted."},{"key":"1_CR15","unstructured":"H. Dierks. Specification and Verification of Polling Real-Time Systems. PhD thesis, Carl von Ossietzky Universit\u00e4t Oldenburg, July 1999."},{"key":"1_CR16","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Proc. of Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1989","unstructured":"David Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In J. Sifakis, editor, Proc. of Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 197\u2013212. Springer-Verlag, 1989."},{"key":"1_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Daws","year":"1998","unstructured":"Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. 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 313\u2013329. Springer-Verlag, 1998."},{"key":"1_CR18","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. IEEE Computer Society Press, December 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"1_CR19","unstructured":"Martijn Hendriks. Devlopment of reactive programs using uppaal. Master\u2019s thesis, KUN, Nijmegen University, 2002."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Martin Hndriks and Kim G. Larsen. Exact acceleration of real-time model checking. In Theory and Practice of Timed Systems, volume 65 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002.","DOI":"10.1016\/S1571-0661(04)80473-0"},{"key":"1_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/3-540-48778-6_17","volume-title":"Proceedings of AMST 1999","author":"K. Havelund","year":"1999","unstructured":"Klaus Havelund, Kim G. Larsen, and Arne Skou. Formal verification of a power controller using the real-time model checker Uppaal. In Proceedings of AMST 1999, volume 1601 of Lecture Notes in Computer Science, pages 277\u2013298, 1999."},{"issue":"8","key":"1_CR22","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM, 21(8):666\u2013677, 1978.","journal-title":"Communications of the ACM"},{"key":"1_CR23","unstructured":"Gerard J. Holzmann. On limits and possibilities of automated protocol analysis. In Proc. 7th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, pages 137\u2013161, 1987."},{"key":"1_CR24","unstructured":"Thomas S. Hune. Modeling a language for embedded systems in timed automata. Technical Report RS-00-17, BRICS, Basic Research in computer Science, August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in FMICS99, pages 259\u2013282."},{"key":"1_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 \u2014Verifying 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":"1_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-45352-0_4","volume-title":"Proceedings of FTRTFT 2000","author":"H. E. Jensen","year":"2000","unstructured":"Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Scaling up Uppaal-automatic verification of real-time systems using compositionality and abstraction. In Proceedings of FTRTFT 2000, volume 1926 of Lecture Notes in Computer Science, pages 19\u201330, 2000."},{"issue":"4","key":"1_CR27","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. Jones","year":"1983","unstructured":"C. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596\u2013620, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR28","doi-asserted-by":"crossref","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.","DOI":"10.1145\/7351.7352"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Fredrik Larsson, 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":"1_CR30","unstructured":"Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Compact data structure and state-space reduction for model-checking real-time systems. Real-Time Systems-the International Journal of Time-Critical Computing Systems, 2002. To appear-accepted for publication."},{"key":"1_CR31","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"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76\u201387. IEEE Computer Society Press, December 1995.","DOI":"10.1109\/REAL.1995.495198"},{"key":"1_CR33","doi-asserted-by":"crossref","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.","DOI":"10.1007\/s100090050010"},{"issue":"3","key":"1_CR34","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":"1_CR35","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989."},{"key":"1_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Proceedings 13th International Conference on Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proceedings 13th International Conference on Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111\u2013125, Madrid, Spain, September 1999."},{"key":"1_CR37","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. In Proceedings First International Workshop on Symbolic Model Checking, volume 23-2 of Electronic Notes in Theoretical Computer Science, Trento, Italy, July 1999."},{"issue":"4","key":"1_CR38","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica, 6(4):319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"1_CR39","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":"1_CR40","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."},{"key":"1_CR41","unstructured":"Tomas Gerhard Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993."},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"D.P.L. Simons and M.I.A. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Springer International Journal of Software Tools for Technology Transfer, 2001.","DOI":"10.1007\/s100090100059"},{"key":"1_CR43","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":"1_CR44","doi-asserted-by":"crossref","unstructured":"Howard Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Standford University, 1995.","DOI":"10.1142\/9789812831583_0007"}],"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-45739-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T01:28:10Z","timestamp":1587518890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45739-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441656","9783540457398"],"references-count":44,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-45739-9_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2002]]}}}