Verifying Large SDL-Specifications Using Model Checking

1. The ATM forum. http://www.atmforum.com/, 2000.

2. D. Bošnački 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’98). Kluwer Academic Publishers, 1998.

   Google Scholar 

3. D. Bošnački, D. Dams, L. Holenderski, and N. Sidorova. Verifying SDL in Spin. In TACAS 2000, LNCS 1785. Springer-Verlag, 2000.

   Google Scholar 

4. 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].

   Google Scholar 

5. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

   Google Scholar 

6. E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, December 1996.

   Google Scholar 

7. 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.

   Google Scholar 

8. A. Barnard F. Regensburger. Formal verification of SDL systems at the Siemens mobile phone department. In Proceedings of TACAS’ 98, LNCS 1384, pages 439–455. Springer-Verlag, 1998.

   Google Scholar 

9. 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’ Formal Description Techniques for Distributed Systems’. Universität Erlangen-Nürnberg, 1996.

   Google Scholar 

10. 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ät zu Berlin, 1998.

    Google Scholar 

11. 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–326. North-Holland, 1989. IFIP TC-6 International Workshop.

    Google Scholar 

12. G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

13. N. Husberg and T. Manner. Emma: Developing an industrial reachability analyser for SDL. In Wing et al. [25], pages 642–662.

    Google Scholar 

14. International Telecommunications Union (ITU), series I recommendations-Integrated services digital networks (ISDN). http://www.itu.int/itudoc/itu-t/rec/i/index.html, 2000.

15. Ph. Leblanc. Simulation, verification and validation of models. white paper. http://www. telelogic.com/download/ObjectGeode/wp simuv.zip, February 1998.

16. L. Ghirvu. M. Bozga, J. Cl. Fernandez. State space reduction based on Live. In Agostino Cortesi and Gilberto Filé, editors, Proceedings of SAS’ 99, LNCS 1694. Springer-Verlag, 1999.

    Google Scholar 

17. Message sequence charts (MSC). ITU-TS Recommendation Z.120, 1996.

    Google Scholar 

18. ObjectGeode 4. http://www.csverilog.com/products/geode.htm, 2000.

19. Specification and Description Language SDL, blue book. CCITT Recommendation Z.100, 1992.

    Google Scholar 

20. 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.

    Google Scholar 

21. N. Sidova and M. Steffen. Embedding chaos. Technical Report TR-ST-01-2, Lehrstuhl für Software-Technologie, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel, March 2000, submitted for publication.

    Google Scholar 

22. Telelogic Malmö AB. SDT 3.1 User Guide and SDT 3.1 Reference Manual, 1997.

    Google Scholar 

23. 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–260. Springer-Verlag, 1999.

    Chapter  Google Scholar 

24. A wireless ATM network demonstrator (WAND), ACTS project AC085. http://www.tik.ee.ethz. ch/~wand/, 1998.

25. J. Wing, J. Woodcock, and J. Davies, editors. Proceedings of Symposium on Formal Methods (FM 99), LNCS 1708. Springer-Verlag, September 1999.

    Google Scholar 

26. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of 13th POPL, pages 184–193. ACM, January 1986.

    Google Scholar 

Download references