{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:40Z","timestamp":1725488620044},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_25","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T19:17:25Z","timestamp":1186600645000},"page":"363-377","source":"Crossref","is-referenced-by-count":18,"title":["Model Checking SDL with Spin"],"prefix":"10.1007","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dennis","family":"Dams","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leszek","family":"Holenderski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natalia","family":"Sidorova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science, 126, pp.183\u2013235, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"D. Bo\u0161na\u010dki, D. Dams, Integrating Real Time into Spin: A Prototype Implementation, S. Budkowski, A. Cavalli, E. Najm, editors, Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE\/PSTV\u201998), Kluwer, 1998. 365, 366","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, J.P. Karimm, L. Mounier, J. Sifakis, If: An Intermediate Representation for SDL and its Applications, In Proc. of SDLFORUM\u2019 99, Montreal, Canada, 1999. 363, 366, 367","DOI":"10.1016\/B978-044450228-5\/50028-X"},{"key":"25_CR4","unstructured":"I. Dravapoulos, N. Pronios, S. Denazis et al., The Magic WAND, Deliverable 3D2, Wireless ATM MAC, September 1997."},{"key":"25_CR5","unstructured":"G. J. Holzmann, Design and Validation of Communication Protocols, Prentice Hall, 1991. Also: http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html 363, 365"},{"key":"25_CR6","unstructured":"G.J. Holzmann, J. Patti, Validating SDL Specification: an Experiment, In E. Brinksma, G. Scollo, Ch.A. Vissers, editors, Protocol Specification, Testing and Verification, Enchede, The Netherlands, 6\u20139 June 1989, pp. 317\u2013326, Amsterdam, 1990. North-Holland. 364, 371"},{"key":"25_CR7","unstructured":"G.J. Holzmann, D. Peled, An Improvement of Formal Verification, PSTV 1994 Conference, Bern, Switzerland, 1994. 366"},{"key":"25_CR8","volume-title":"System Engineering Using SDL-92","author":"A. Olsen","year":"1997","unstructured":"A. Olsen et al., System Engineering Using SDL-92, Elsevier Science, North-Holland, 1997. 363"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"D. Peled, Combining Partial Order Reductions with On-the-Fly Model Checking, Computer Aided Verification CAV 94, LCNS 818, pp. 377\u2013390, 1994. 366","DOI":"10.1007\/3-540-58179-0_69"},{"key":"25_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/3-540-48234-2_19","volume-title":"6th Int. SPIN Workshop","author":"H. Tuominen","year":"1999","unstructured":"H. Tuominen, Embedding a Dialect of SDL in PROMELA, 6th Int. SPIN Workshop, LNCS 1680, pp. 245\u2013260, 1999. 364, 371, 372"},{"key":"25_CR11","unstructured":"Verilog, ObjectGEODE tutorial, Version 1.2, Verilog SA, Toulouse, France, 1996. 364, 366, 369"},{"key":"25_CR12","unstructured":"VIRES, Verifying Industrially Relevant Systems, Esprit Long Term Research Project #23498, http:\/\/radon.ics.ele.tue.nl\/~vires , 1996. 367"},{"key":"25_CR13","unstructured":"WAND consortium, Magic WAND-Wireless ATM Network Demonstrator, http:\/\/www.tik.ee.ethz.ch\/~wand , 1996. 364, 373"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T17:07:12Z","timestamp":1556730432000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}