Skip to main content
SpringerLink
Log in

I/O Efficient Directed Model Checking

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3385))

Abstract

Directed model checking has proved itself to be a useful technique in reducing the state space of the problem graph. But still, its potential is limited by the available memory. This problem can be circumvented by the use of secondary storage devices to store the state space. This paper discusses directed best-first search to enhance error detection capabilities of model checkers like SPIN by using a streamed access to secondary storage. We explain, how to extend SPIN to allow external state access, and how to adapt heuristic search algorithms to ease error detection for this case. We call our derivate IO-HSF-SPIN. In the theoretical part of the paper, we extend the heuristic-based external searching algorithm to general weighted and directed graphs. We conduct experiments with some challenging protocols in Promela syntax like GIOP and dining philosophers and have succeeded in solving some hard instances externally.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bérard, B., Bidoit, A.F.M., Laroussine, F., Petit, A., Petrucci, L., Schoenebelen, P., McKenzie, P.: Systems and Software Verification. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  2. Burch, J.R., Clarke, E.M., McMillian, K.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  3. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  4. Dijkstra, E.W.: A note on two problems in connection with graphs. Numerische Mathematik 1, 269–271 (1959)

    Article  MATH  MathSciNet  Google Scholar 

  5. Edelkamp, S., Jabbar, S., Schroedl, S.: External A*. In: Biundo, S., Frühwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol. 3238, pp. 226–240. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology, STTT (2004)

    Google Scholar 

  7. Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: Herzog, O. (ed.) KI 1998. LNCS, vol. 1504, pp. 81–92. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  8. Edelkamp, S., Schrödl, S.: Localizing A*. In: National Conference on Artificial Intelligence (AAAI), pp. 885–890 (2000)

    Google Scholar 

  9. Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics 4, 100–107 (1968)

    Article  Google Scholar 

  10. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1990)

    Google Scholar 

  11. Jensen, R.M., Bryant, R.E., Veloso, M.M.: SetA*: An efficient BDD-based heuristic search algorithm. In: National Conference on Artificial Intelligence, AAAI (2002)

    Google Scholar 

  12. Kamel, M., Leue, S.: Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. International Journal on Software Tools for Technology Transfer 2(4), 394–409 (2000)

    Article  MATH  Google Scholar 

  13. Korf, R.: Best-first frontier search with delayed duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 650–657 (2004)

    Google Scholar 

  14. Korf, R.E.: Breadth-first frontier search with delayed duplicate detection. In: Workshop on Model Checking and Artificial Intelligence (MoChArt), pp. 87–92 (2003)

    Google Scholar 

  15. Lluch-Lafuente, A.: Symmetry reduction and heuristic search for error detection in model checking. In: Model Checking and Artificial Intelligence, MoChArt 2003 (2003)

    Google Scholar 

  16. Lluch-Lafuente, A., Edelkamp, S., Leue, S.: Partial order reduction in directed model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 112–127. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Mehlhorn, K., Meyer, U.: External-memory breadth-first search with sublinear I/O. In: Möhring, R.H., Raman, R. (eds.) ESA 2002. LNCS, vol. 2461, pp. 723–735. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Meyer, U., Sanders, P., Sibeyn, J.: Memory Hierarchies. Springer, Heidelberg (2003)

    Book  MATH  Google Scholar 

  19. Munagala, K., Ranade, A.: I/O-complexity of graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 87–88 (2001)

    Google Scholar 

  20. Sawatzki, D.: Experimental studies of symbolic shortest-path algorithms. In: Workshop on Algorithm Engineering (WAE), pp. 482–497 (2004)

    Google Scholar 

  21. Sawatzki, D.: A symbolic approach to the all-pairs shortest-paths problem. In: Workshop on Algorithm Engineering (WAE), pp. 482–497 (2004)

    Google Scholar 

  22. Sibeyn, J.F.: External matrix multiplication and all-pairs shortest path. Information Processing Letters 91(2), 99–106 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  23. Stern, U., Dill, D.: Using magnetic disk instead of main memory in the murphi verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Zhou, R., Hansen, E.: Breadth-first heuristic search. In: International Conference on Automated Planning and Scheduling (ICAPS), pp. 92–100 (2004)

    Google Scholar 

  25. Zhou, R., Hansen, E.: Structured duplicate detection in external-memory graph search. In: National Conference on Artificial Intelligence (AAAI), pp. 683–689 (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Dortmund, Baroper Str. 301, Dortmund, Germany

    Shahid Jabbar & Stefan Edelkamp

Authors
  1. Shahid Jabbar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS, Paris, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jabbar, S., Edelkamp, S. (2005). I/O Efficient Directed Model Checking. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30579-8_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-24297-0

  • Online ISBN: 978-3-540-30579-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation