Synchronous Closing of Timed SDL Systems for Model Checking

1. 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’ 98, volume 1427 of Lecture Notes in Computer Science, pages 521–525. Springer-Verlag, 1998.

   Google Scholar 

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

   Google Scholar 

3. D. Bošnački, 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.

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

   Google Scholar 

5. 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’00, 2000.

   Google Scholar 

6. J. Brock and W. Ackerman. An anomaly in the specifications of nondeterministic packet systems. Technical Report Computation Structures Group Note CSG-33, MIT Lab. for Computer Science, Nov. 1977.

   Google Scholar 

7. E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994. A preliminary version appeared in the Proceedings of POPL 92.

   Article  Google Scholar 

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

   Google Scholar 

9. D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstraction preserving ∀CTL*,∃CTL*, and CTL*. In E.-R. Olderog, editor, Proceedings of PROCOMET’ 94. IFIP, North-Holland, June 1994.

   Google Scholar 

10. P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Computer Aided Verification 1990, volume 531 of Lecture Notes in Computer Science, pages 176–449. Springer-Verlag, 1991. an extended Version appeared in ACM/AMS DIMACS Series, volume 3, pages 321-340, 1991.

    Chapter  Google Scholar 

11. M. S. Hecht. Flow Analysis of Programs. North-Holland, 1977.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

14. G. Kildall. A unified approach to global program optimization. In Proceedings of POPL’ 73, pages 194–206. ACM, January 1973.

    Google Scholar 

15. O. Kupferman and M. Y. Vardi. Module checking revisited. In O. Grumberg, editor, CAV’ 97, Proceedings of the 9th International Conference on Computer-Aided Verification, Haifa. Israel, volume 1254 of Lecture Notes in Computer Science. Springer, June 1997.

    Google Scholar 

16. O. Kupferman, M. Y. Vardi, and P. Wolper. Module checking. In R. Alur, editor, Proceedings of CAV’ 96, volume 1102 of Lecture Notes in Computer Science, pages 75–86, 1996.

    Google Scholar 

17. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Twelfth Annual Symposium on Principles of Programming Languages (POPL) (New Orleans, LA), pages 97–107. ACM, January 1985.

    Google Scholar 

18. D. Long. Model Checking, Abstraction and Compositional Verification. PhD thesis, Carnegie Mellon University, 1993.

    Google Scholar 

19. F. Nielson, H.-R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

20. A. Pnueli. The temporal logic of programs. In Proceeding of the 18th Annual Symposium on Foundations of Computer Science, pages 45–57, 1977.

    Google Scholar 

21. N. Sidorova and M. Steffen. Embedding chaos. In P. Cousot, editor, Proceedings of the 8th Static Analysis Symposium (SAS’01), volume 2126 of Lecture Notes in Computer Science, pages 319–334. Springer-Verlag, 2001.

    Google Scholar 

22. 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–416. Springer-Verlag, Feb. 2001.

    Google Scholar 

23. A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1992. Earlier version in the proceeding of CAV’ 90 Lecture Notes in Computer Science 531, Springer-Verlag 1991, pp. 156–165 and in Computer-Aided Verification’ 90, DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 3, AMS & ACM 1991, pp. 25-41.

    Google Scholar 

Download references