{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:39Z","timestamp":1725573879407},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_29","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"504-522","source":"Crossref","is-referenced-by-count":1,"title":["Analyzing the Redesign of a Distributed Lift System in UPPAAL"],"prefix":"10.1007","author":[{"given":"Jun","family":"Pang","sequence":"first","affiliation":[]},{"given":"Bart","family":"Karstens","sequence":"additional","affiliation":[]},{"given":"Wan","family":"Fokkink","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Aceto","year":"1998","unstructured":"Aceto, L., Burgueno, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 263\u2013280. Springer, Heidelberg (1998)"},{"issue":"2","key":"29_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/S1567-8326(02)00036-X","volume":"52-53","author":"J. Bengtsson","year":"2002","unstructured":"Bengtsson, J., Griffioen, W.O.D., Kristoffersen, K.J., Larsen, K.G., Larsson, F., Pettersson, P., Wang, Y.: Automated analysis of an audio control protocol using UPPAAL. Journal of Logic and Algebraic Programming\u00a052-53, 163\u2013181 (2002)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"29_CR4","first-page":"109","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Computation\u00a060, 109\u2013137 (1984)","journal-title":"Information and Computation"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"Computer Aided Verification","author":"S.C.C. Blom","year":"2001","unstructured":"Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I.A., Lisser, B., van de Pol, J.C.: \u03bcCRL: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 250\u2013254. Springer, Heidelberg (2001)"},{"unstructured":"Gmbh, R.B.: Postfach 30 02 40, D-70442 Stuttgart, Germany. CAN Specification. Version 2.0 (1991)","key":"29_CR6"},{"issue":"1\/2","key":"29_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S1567-8326(02)00038-3","volume":"55","author":"J.F. Groote","year":"2003","unstructured":"Groote, J.F., Pang, J., Wouters, A.G.: Analysis of a distributed system for lifting trucks. Journal of Logic and Algebraic Programming\u00a055(1\/2), 21\u201356 (2003)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"29_CR8","series-title":"Workshops in Computing Series","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/978-1-4471-2120-6_2","volume-title":"Algebra of Communicating Processes 1994,","author":"J.F. Groote","year":"1995","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of \u03bcCRL. In: Algebra of Communicating Processes 1994, Workshops in Computing Series, pp. 26\u201362. Springer, Heidelberg (1995)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","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","author":"K. Havelund","year":"1999","unstructured":"Havelund, K., Larsen, K.G., Skou, A.: Formal verification of a power controller using the real-time model checker UPPAAL. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 277\u2013298. Springer, Heidelberg (1999)"},{"unstructured":"Karstens, B.: Formal verification of the redesign of a distributed lift system using UPPAAL. Master thesis, Utrecht University (2003), Available at http:\/\/www.cwi.nl\/~pangjun\/research\/liftredesign.ps","key":"29_CR10"},{"issue":"1-2","key":"29_CR11","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"3","key":"29_CR12","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s100090100048","volume":"3","author":"M. Lindahl","year":"2001","unstructured":"Lindahl, M., Pettersson, P., Wang, Y.: Formal design and analysis of a gear controller. International Journal on Software Tools for Technology Transfer\u00a03(3), 353\u2013368 (2001)","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T11:02:38Z","timestamp":1592218958000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}