{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:53Z","timestamp":1725484133911},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_30","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:45:28Z","timestamp":1179362728000},"page":"531-548","source":"Crossref","is-referenced-by-count":5,"title":["Closing Open SDL-Systems for Model Checking with DTSpin"],"prefix":"10.1007","author":[{"given":"Natalia","family":"Ioustinova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natalia","family":"Sidorova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"unstructured":"Telelogic TAU SDL Suite. \n                  http:\/\/www.telelogic.com\/products\/sdl\/\n                  \n                , 2002.","key":"30_CR1"},{"key":"30_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Proceedings of CAV\u2019 98","author":"R. Alur","year":"1998","unstructured":"R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha: Modularity in model checking. In A. J. Hu and M. Y. Vardi, editors, Proceedings of CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, pages 521\u2013525. Springer-Verlag, 1998."},{"doi-asserted-by":"crossref","unstructured":"D. Bo\u0161na\u010dki and D. Dams. Integrating real time into Spin: A prototype implementation. In S. Budkowski, A. Cavalli, and E. Najm, editors, Proceedings of Formal Description Techniques and Protocol Specification, Testing, and Verification (FORTE\/PSTV\u201998). Kluwer Academic Publishers, 1998.","key":"30_CR3","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"30_CR4","series-title":"Lect Notes Comput Sci","volume-title":"TACAS 2000","author":"D. Bo\u0161na\u010dki","year":"2000","unstructured":"D. Bo\u0161na\u010dki, D. Dams, L. Holenderski, and N. Sidorova. Verifying SDL in Spin. In S. Graf and M. Schwartzbach, editors, TACAS 2000, volume 1785 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"30_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Symposium on Formal Methods (FM 99)","author":"M. Bozga","year":"1999","unstructured":"M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J.-P. Krimm, and L. Mounier. IF: An intermediate representation and validation environment for timed asynchronous systems. In J. Wing, J. Woodcock, and J. Davies, editors, Proceedings of Symposium on Formal Methods (FM 99), volume 1708 of Lecture Notes in Computer Science. Springer-Verlag, Sept. 1999."},{"key":"30_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u2019 00","author":"M. Bozga","year":"2000","unstructured":"M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J.-P. Krimm, and L. Mounier. IF: A validation environment for timed asynchronous systems. In E. A. Emerson and A. P. Sistla, editors, Proceedings of CAV\u2019 00, volume 1855 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"unstructured":"M. Bozga, S. Graf, A. Kerbrat, L. Mounier, I. Ober, and D. Vincent. SDL for real-time: What is missing? In Y. Lahav, S. Graf, and C. Jard, editors, Electronic Proceedings of SAM\u201900, 2000.","key":"30_CR7"},{"issue":"5","key":"30_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, 1994. A preliminary version appeared in the Proceedings of POPL 92.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"30_CR9","series-title":"Lect Notes Comput Sci","first-page":"244","volume-title":"Proceedings of the Workshop on Logic of Programs 1981","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic specifications. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs 1981, volume 131 of Lecture Notes in Computer Science, pages 244\u2013263. Springer-Verlag, 1982."},{"unstructured":"E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, Dec. 1996. Available also as Carnegie Mellon University technical report CMU-CS-96-178.","key":"30_CR10"},{"doi-asserted-by":"crossref","unstructured":"C. Colby, P. Godefroid, and L. J. Jagadeesan. Automatically closing of open reactive systems. In Proceedings of 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 1998.","key":"30_CR11","DOI":"10.1145\/277650.277754"},{"doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximaton of fixpoints. In Fourth Annual Symposium on Principles of Programming Languages (POPL) (Los Angeles, Ca), pages 238\u2013252. ACM, January 1977.","key":"30_CR12","DOI":"10.1145\/512950.512973"},{"unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstraction preserving \u2200CTL*,\u2203CTL*, and CTL*. In E.-R. Olderog, editor, Proceedings of PROCOMET\u2019 94. IFIP, North-Holland, June 1994.","key":"30_CR13"},{"unstructured":"Discrete-time Spin. \n                  http:\/\/win.tue.nl\/dragan\/DTSpin.html\n                  \n                , 2000.","key":"30_CR14"},{"unstructured":"M. Dwyer and D. Schmidt. Limiting state explosion with filter-based refinement. In Proceedings of the 1st International Workshop in Verification, Abstract Interpretation, and Model Checking, Oct. 1997.","key":"30_CR15"},{"unstructured":"M. B. Dwyer and J. Hatcliff. Slicing software for model construction. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201999), Jan. 1999.","key":"30_CR16"},{"doi-asserted-by":"crossref","unstructured":"M. B. Dwyer and C. S. Pasareanu. Filter-based model checking of partial systems. In Proceedings of the 6th ACM SIGSOFT Symposium on the Foundations of Software Engineering (SIGSOFT\u2019 98), pages 189\u2013202, 1998.","key":"30_CR17","DOI":"10.1145\/288195.288307"},{"key":"30_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1007\/BFb0054188","volume-title":"Proceedings of TACAS\u2019 98","author":"A. B. F. Regensburger","year":"1998","unstructured":"A. B. F. Regensburger. Formal verification of SDL systems at the Siemens mobile phone department. In B. Steffen, editor, Proceedings of TACAS\u2019 98, number 1384 in Lecture Notes in Computer Science, pages 439\u2013455. Springer-Verlag, 1998."},{"key":"30_CR19","series-title":"Lect Notes Comput Sci","first-page":"123","volume-title":"Model Checking Software, Proceedings of the 8th International SPIN Workshop (SPIN 2001), Toronto, Canada","author":"J. Guoping","year":"2001","unstructured":"J. Guoping and S. Graf. Verification experiments on the Mascara protocol. In M. B. Dwyer, editor, Model Checking Software, Proceedings of the 8th International SPIN Workshop (SPIN 2001), Toronto, Canada, Lecture Notes in Computer Science, pages 123\u2013142. Springer-Verlag, 2001."},{"unstructured":"M. S. Hecht. Flow Analysis of Programs. North-Holland, 1977.","key":"30_CR20"},{"unstructured":"U. Hinkel. Verification of SDL specifications on the basis of stream semantics. In Y. Lahav, A. Wolisz, J. Fischer, and E. Holz, editors, Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC (SAM\u201998), pages 241\u2013250, 1998.","key":"30_CR21"},{"unstructured":"G. Holzmann and J. Patti. Validating SDL specifications: an experiment. In E. Brinksma, editor, International Workshop on Protocol Specification, Testing and Verification IX (Twente, The Netherlands), pages 317\u2013326. North-Holland, 1989. IFIP TC-6 International Workshop.","key":"30_CR22"},{"unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.","key":"30_CR23"},{"doi-asserted-by":"crossref","unstructured":"G. Kildall. A unified approach to global program optimization. In Proceedings of POPL\u2019 73, pages 194\u2013206. ACM, January 1973.","key":"30_CR24","DOI":"10.1145\/512927.512945"},{"key":"30_CR25","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u2019 97, Proceedings of the 9th International Conference on Computer-Aided Verification, Haifa. Israel","author":"O. Kupferman","year":"1997","unstructured":"O. Kupferman and M. Y. Vardi. Module checking revisited. In O. Grumberg, editor, CAV\u2019 97, Proceedings of the 9th International Conference on Computer-Aided Verification, Haifa. Israel, volume 1254 of Lecture Notes in Computer Science. Springer, June 1997."},{"key":"30_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Proceedings of CAV\u2019 96","author":"O. Kupferman","year":"1996","unstructured":"O. Kupferman, M. Y. Vardi, and P. Wolper. Module checking. In R. Alur, editor, Proceedings of CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, pages 75\u201386, 1996."},{"key":"30_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of SAS\u2019 99","author":"L. G. M. Bozga","year":"1999","unstructured":"L. G. M. Bozga, J. Cl. Fernandez. State space reduction based on Live. In A. Cortesi and G. Fil\u00e9, editors, Proceedings of SAS\u2019 99, volume 1694 of Lecture Notes in Computer Science. Springer-Verlag, 1999."},{"unstructured":"L. I. Millet and T. Teitelbaum. Slicing promela and its application to model checking, simulation, and protocol understanding. In E. Najm, A. Serhrouchni, and G. Holzmann, editors, Electronic Proceedings of the Fourth International SPIN Workshop, Paris, France, Nov. 1998.","key":"30_CR28"},{"doi-asserted-by":"crossref","unstructured":"F. Nielson, H.-R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.","key":"30_CR29","DOI":"10.1007\/978-3-662-03811-6"},{"unstructured":"ObjectGeode 4. \n                  http:\/\/www.csverilog.com\/products\/geode.htm\n                  \n                , 2000.","key":"30_CR30"},{"key":"30_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the 5th International Symposium on Programming 1981","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In M. Dezani-Ciancaglini and U. Montanari, editors, Proceedings of the 5th International Symposium on Programming 1981, volume 137 of Lecture Notes in Computer Science, pages 337\u2013351. Springer-Verlag, 1982."},{"key":"30_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/3-540-47764-0_18","volume-title":"Proceedings of the 8th Static Analysis Symposium (SAS\u201901)","author":"N. Sidorova","year":"2001","unstructured":"N. Sidorova and M. Steffen. Embedding chaos. In P. Cousot, editor, Proceedings of the 8th Static Analysis Symposium (SAS\u201901), volume 2126 of Lecture Notes in Computer Science, pages 319\u2013334. Springer-Verlag, 2001."},{"key":"30_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/3-540-48213-X_25","volume-title":"Proceedings of the 10th International SDL Forum SDL 2001: Meeting UML","author":"N. Sidorova","year":"2001","unstructured":"N. Sidorova and M. Steffen. Verifying large SDL-specifications using model checking. In R. Reed and J. Reed, editors, Proceedings of the 10th International SDL Forum SDL 2001: Meeting UML, volume 2078 of Lecture Notes in Computer Science, pages 403\u2013416. Springer-Verlag, Feb. 2001."},{"key":"30_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-47813-2_6","volume-title":"Proceedings of the hird International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2002","author":"N. Sidorova","year":"2002","unstructured":"N. Sidorova and M. Steffen. Synchronous closing of timed SDL systems for model checking. In A. Cortesi, editor, Proceedings of the hird International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2002, volume 2294 of Lecture Notes in Computer Science, pages 79\u201393. Springer-Verlag, 2002."},{"key":"30_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-48234-2_19","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking, Proceedings of 5th and 6th International SPIN Workshops, Trento\/Toulouse","author":"H. Tuominen","year":"1999","unstructured":"H. Tuominen. Embedding a dialect of SDL in Promela. In D. Dams, R. Gerth, S. Leue, and M. Massink, editors, Theoretical and Practical Aspects of SPIN Model Checking, Proceedings of 5th and 6th International SPIN Workshops, Trento\/Toulouse, volume 1680 of Lecture Notes in Computer Science, pages 245\u2013260. Springer-Verlag, 1999."},{"unstructured":"A wireless ATM network demonstrator (WAND), ACTS project AC085. \n                  http:\/\/www.tik.ee.ethz.ch\/wand\/\n                  \n                , 1998.","key":"30_CR36"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T10:40:49Z","timestamp":1547721649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}