{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:58:16Z","timestamp":1725487096553},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422815"},{"type":"electronic","value":"9783540482130"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48213-x_25","type":"book-chapter","created":{"date-parts":[[2007,7,2]],"date-time":"2007-07-02T14:01:14Z","timestamp":1183384874000},"page":"403-420","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Large SDL-Specifications Using Model Checking"],"prefix":"10.1007","author":[{"given":"Natalia","family":"Sidorova","sequence":"first","affiliation":[]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,22]]},"reference":[{"key":"25_CR1","unstructured":"The ATM forum. http:\/\/www.atmforum.com\/ , 2000."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"D. Bo\u0161na\u010dki and D. Dams. Integrating real time into Spin: A prototype implementation. In Proceedings of Formal Description Techniques and Protocol Specification, Testing, and Verification (FORTE\/PSTV\u201998). Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"25_CR3","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 TACAS 2000, LNCS 1785. Springer-Verlag, 2000."},{"key":"25_CR4","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 Wing et al. [25]."},{"key":"25_CR5","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, December 1996.","DOI":"10.1145\/242223.242257"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, Los Angeles, CA. ACM, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"25_CR8","series-title":"Lect Notes Comput Sci","first-page":"439","volume-title":"Proceedings of TACAS\u2019 98","author":"A. Barnard","year":"1998","unstructured":"A. Barnard F. Regensburger. Formal verification of SDL systems at the Siemens mobile phone department. In Proceedings of TACAS\u2019 98, LNCS 1384, pages 439\u2013455. Springer-Verlag, 1998."},{"key":"25_CR9","unstructured":"J. Grabowski, R. Scheurer, D. Toggweiler, and D. Hogrefe. Dealing with the complexity of state space exploration algorithms. In Proceedings of the 6th GI\/ITG technical meeting on\u2019 Formal Description Techniques for Distributed Systems\u2019. Universit\u00e4t Erlangen-N\u00fcrnberg, 1996."},{"key":"25_CR10","unstructured":"U. Hinkel. Verification of SDL specifications on the basis of stream semantics. In Y. Lahav, A. Wolisz, J. Fischer, and E. Holz, editors, Proc. of the 1st Workshop of the SDL Forum Society on SDL and MSC. Humboldt-Universit\u00e4t zu Berlin, 1998."},{"key":"25_CR11","unstructured":"G. Holzmann and J. Patti. Validating SDL specifications: an experiment. In Ed 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":"25_CR12","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"N. Husberg and T. Manner. Emma: Developing an industrial reachability analyser for SDL. In Wing et al. [25], pages 642\u2013662.","DOI":"10.1007\/3-540-48119-2_36"},{"key":"25_CR14","unstructured":"International Telecommunications Union (ITU), series I recommendations-Integrated services digital networks (ISDN). http:\/\/www.itu.int\/itudoc\/itu-t\/rec\/i\/index.html , 2000."},{"key":"25_CR15","unstructured":"Ph. Leblanc. Simulation, verification and validation of models. white paper. http:\/\/www. telelogic.com\/download\/ObjectGeode\/wp simuv.zip , February 1998."},{"key":"25_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of SAS\u2019 99","author":"L. Ghirvu","year":"1999","unstructured":"L. Ghirvu. M. Bozga, J. Cl. Fernandez. State space reduction based on Live. In Agostino Cortesi and Gilberto Fil\u00e9, editors, Proceedings of SAS\u2019 99, LNCS 1694. Springer-Verlag, 1999."},{"key":"25_CR17","unstructured":"Message sequence charts (MSC). ITU-TS Recommendation Z.120, 1996."},{"key":"25_CR18","unstructured":"ObjectGeode 4. http:\/\/www.csverilog.com\/products\/geode.htm , 2000."},{"key":"25_CR19","unstructured":"Specification and Description Language SDL, blue book. CCITT Recommendation Z.100, 1992."},{"key":"25_CR20","series-title":"Technical Report TR-97-18","volume-title":"SDL specification and verification of a distributed access generic optical network interface for SMDS networks","author":"S. M. Shahrier","year":"1997","unstructured":"S. M. Shahrier and R. M. Jenevein. SDL specification and verification of a distributed access generic optical network interface for SMDS networks. Technical Report TR-97-18, University of Texas at Austin, Department of Computer Sciences, July 1997."},{"key":"25_CR21","unstructured":"N. Sidova and M. Steffen. Embedding chaos. Technical Report TR-ST-01-2, Lehrstuhl f\u00fcr Software-Technologie, Institut f\u00fcr Informatik und praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, March 2000, submitted for publication."},{"key":"25_CR22","unstructured":"Telelogic Malm\u00f6 AB. SDT 3.1 User Guide and SDT 3.1 Reference Manual, 1997."},{"key":"25_CR23","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","author":"H. Tuominen","year":"1999","unstructured":"H. Tuominen. Embedding a dialect of SDL in Promela. In Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink, editors, Theoretical and Practical Aspects of SPIN Model Checking, Proceedings of 5th and 6th Internaional SPIN Workshops, Trento\/Toulouse, LNCS 1680, pages 245\u2013260. Springer-Verlag, 1999."},{"key":"25_CR24","unstructured":"A wireless ATM network demonstrator (WAND), ACTS project AC085. http:\/\/www.tik.ee.ethz. ch\/~wand\/ , 1998."},{"key":"25_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Symposium on Formal Methods (FM 99)","year":"1999","unstructured":"J. Wing, J. Woodcock, and J. Davies, editors. Proceedings of Symposium on Formal Methods (FM 99), LNCS 1708. Springer-Verlag, September 1999."},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of 13th POPL, pages 184\u2013193. ACM, January 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","SDL 2001: Meeting UML"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48213-X_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T21:36:06Z","timestamp":1556573766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48213-X_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422815","9783540482130"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48213-x_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}