{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:17Z","timestamp":1740028757167,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_20","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"278-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["\u221aerics: A Tool for Verifying Timed Automata and Estelle Specifications"],"prefix":"10.1007","author":[{"given":"Piotr","family":"Dembi\u0144ski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agata","family":"Janowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pawe\u0142","family":"Janowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agata","family":"P\u00f3\u0142rola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Szreter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo\u017cena","family":"Wo\u017ana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"20_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata for modelling real-time systems","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the International Colloquium on Automata, Languages and Programming (ICALP\u201990), volume 443 of LNCS, pages 322\u2013335. Springer-Verlag, 1990."},{"key":"20_CR2","unstructured":"J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of Uppaal. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998."},{"key":"20_CR3","unstructured":"D. Beyer. Rabbit: Verification of real-time systems. In Proc. of the Workshop on Real-Time Tools (RT-TOOLS\u201901), pages 13\u201321, 2001."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. IF: An intermediate representation for SDL and its applications. In Proc. of SDL Forum\u201999, pages 423\u2013440, 1999.","DOI":"10.1016\/B978-044450228-5\/50028-X"},{"key":"20_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"NuSMV 2: An open-source tool for symbolic model checking","author":"A. Cimatti","year":"2002","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An open-source tool for symbolic model checking. In Proc. of CAV\u201902, volume 2404 of LNCS, pages 359\u2013364. Springer-Verlag, 2002."},{"key":"20_CR6","unstructured":"A. Doro\u015b, A. Janowska, and P. Janowski. From specification languages to Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P\u201902), volume 161(1) of Informatik-Berichte, pages 117\u2013128. Humboldt University, 2002."},{"key":"20_CR7","unstructured":"H. Garavel, F. Lang, and R. Mateescu. An overview of CADP 2001. Technical Report RT-254, INRIA Rh\u00f4ne-Alpes, 655, avenue de l\u2019Europe, 38330 Montbonnot-St-Martin, December 2001."},{"issue":"5","key":"20_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Eng., 23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Eng."},{"key":"20_CR9","unstructured":"ISO 8807 \u2014 information processing systems-Open System Interconnection. LOTOS \u2014 a formal description technique based on the temporal ordering of observational behaviour, 1989."},{"key":"20_CR10","unstructured":"ISO\/IEC 9074(E), Estelle-a formal description technique based on an extended state-transition model. International Standards Organization, 1997."},{"key":"20_CR11","unstructured":"ITU-T Recommendation Z.100(11\/99): Languages for telecommunication applications \u2014 Specification and Description Language, 1999."},{"key":"20_CR12","unstructured":"K. McMillan. The SMV system. Technical Report CMU-CS-92-131, Carnegie-Mellon University, February 1992."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Cha.: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC\u201901), pages 530\u2013535, June 2001.","DOI":"10.1145\/378239.379017"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"W. Penczek, B. Wo\u017ana, and A. Zbrzezny. SAT-based bounded model checking for the universal fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01-237 Warsaw, August 2002.","DOI":"10.1007\/3-540-45739-9_17"},{"key":"20_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-45739-9_17","volume-title":"Towards bounded model checking for the universal fragment of TCTL","author":"W. Penczek","year":"2002","unstructured":"W. Penczek, B. Wo\u017ana, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT\u201902), volume 2469 of LNCS, pages 265\u2013288. Springer-Verlag, 2002."},{"key":"20_CR16","first-page":"40","volume":"70","author":"P. Pettersson","year":"Uppaal2k","unstructured":"P. Pettersson and K. G. Larsen. Uppaal2k. Bulletin of the European Association for Theoretical Computer Science, 70:40\u201344, February 2000.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"20_CR17","unstructured":"A. P\u00f3\u0142rola, W. Penczek, and M. Szreter. Reachability analysis for Timed Automata based on partitioning. Technical report, ICS PAS, Ordona 21, 01-237 Warsaw, 2003. to appear."},{"key":"20_CR18","unstructured":"R. Sebastiani. Integrating SAT solvers with math reasoners: Foundations and basic algorithms. Technical Report 0111-22, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy, November 2001."},{"key":"20_CR19","unstructured":"B. Wo\u017ana, W. Penczek, and A. Zbrzezny. Checking reachability properties for Timed Automata via SAT. Technical Report 949, ICS PAS, Ordona 21, 01-237 Warsaw, October 2002."},{"key":"20_CR20","unstructured":"B. Wo\u017ana, W. Penczek, and A. Zbrzezny. Reachability for timed systems based on SAT-solvers. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P\u201902), volume 161(2) of Informatik-Berichte, pages 380\u2013395. Humboldt University, 2002."},{"issue":"1\/2","key":"20_CR21","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"S. Yovine. KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1(1\/2):123\u2013133, 1997.","journal-title":"Springer International Journal of Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:12:33Z","timestamp":1739992353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}