Skip to main content
SpringerLink
Log in

Efficient Path Finding with the Sweep-Line Method Using External Storage

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2885))

Included in the following conference series:

Abstract

The sweep-line method deletes states on-the-fly during state space exploration to reduce peak memory usage. This deletion of states prohibits the immediate generation of, e.g., an error-trace when the violation of a safety property is detected. We address this problem by combining the sweep-line method with storing a spanning tree of the explored state space in external storage on a magnetic disk. We show how this allows us to easily obtain paths in the state space, such as error-traces. A key property of the proposed technique is that it avoids searching in external storage during the state space exploration and gives the same reduction in peak memory usage as the stand-alone sweep-line method. We evaluate the proposed technique on a number of example systems, and compare its performance to a related technique. These practical experiments demonstrate how the suggested technique complements existing techniques based on using external storage.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Design/CPN, http://www.daimi.au.dk/designCPN

  2. Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimaility in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)

    Article  Google Scholar 

  5. Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  7. Clarke, E.M., Filkorn, T., Jha, S.: Exploiting Symmetries in Temporal Logic Model Checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450–462. Springer, Heidelberg (1993)

    Google Scholar 

  8. Emerson, E.A., Jha, S., Peled, D.: Combining Partial Order and Symmetry Reduction. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 35–49. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  9. Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design 9(1/2), 105–131 (1996)

    Article  Google Scholar 

  10. Fehnker, A.: Scheduling a Steel Plant with Timed Automata. In: Proc. of RTCSA 1999, pp. 280–286. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

  11. WAP Forum. WAP Wireless Transaction Protocol Specification. June 2000 Conformance Release. Available via: http://www.wapforum.org/ (February 19, 2000)

  12. WAP Forum. Wireless Application Protocol. Specifications available via: http://www.wapforum.org/

  13. Godefroid, P., Holzmann, G.J., Pirottin, D.: State-Space Caching Revisited. Formal Methods in System Design 7(3), 227–241 (1995)

    Article  Google Scholar 

  14. Gordon, S., Kristensen, L.M., Billington, J.: Verification of a Revised WAP Wireless Transaction Protocol. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 182–202. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Holzmann, G.J.: Tracing Protocols. Bell System Technical Journal 64, 2413–2434 (1985)

    Google Scholar 

  16. Holzmann, G.J.: An Improved Protocol Reachability Analysis Technique. Software, Practice and Experience 18(2), 137–161 (1988)

    Article  Google Scholar 

  17. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall International, Englewood Cliffs (1991)

    Google Scholar 

  18. Holzmann, G.J.: An Analysis of Bitstate Hashing. Formal Methods in System Design 13, 289–307 (1998)

    Article  Google Scholar 

  19. Ip, C.N., Dill, D.L.: Better Verification Through Symmetry. Formal Methods in System Design 9(1/2), 41–75 (1996)

    Google Scholar 

  20. Jard, C., Jeron, T.: Bounded-memory Algorithms for Verification On-the-fly. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 192–202. Springer, Heidelberg (1992)

    Google Scholar 

  21. Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. Basic Concepts, vol. 1. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  22. Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9(1/2), 7–40 (1996)

    Article  Google Scholar 

  23. Katz, S., Miller, H.: Saving Space by Fully Exploiting Invisible Transitions. Formal Methods in System Design 14, 311–332 (1999)

    Article  Google Scholar 

  24. Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)

    Article  MATH  Google Scholar 

  25. Kristensen, L.M., Mailund, T.: A Generalised Sweep-Line Method for Safety Properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Kristensen, L.M., Mailund, T.: A Compositional Sweep-Line State Space Exploration Method. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 327–343. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  27. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  28. Milner, R.: Communication and Concurrency. Prentice-Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  29. Parashkevov, A.N., Yantchev, J.: Space Efficient Reachability Analysis through use of Pseudo-root States. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 50–64. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  30. Peled, D.: All from One, One for All: On Model Checking Using Representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)

    Google Scholar 

  31. Reisig, W.: Petri Nets. EACTS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)

    MATH  Google Scholar 

  32. Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)

    Google Scholar 

  33. Stern, U., Dill, D.L.: A New Scheme for Memory-Efficient Probabilistic Verification. In: Proc. of Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pp. 333–348 (1996)

    Google Scholar 

  34. Stern, U., Dill, D.L.: Combining State Space Caching and Hash Compaction. In: 4. GI/ITG/GME Workshop zur Methoden des Entwurfs und der Verifikation Digitaler Systeme, Kreischa, pp. 81–90. Shaker, Aachen (1996)

    Google Scholar 

  35. Stern, U., Dill, D.L.: 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 

  36. Ullman, J.D.: Elements of ML Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  37. Valmari, A.: A Stubborn Attack on State Explosion. In Proceedings of CAV’90. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  38. Valmari, A.: Stubborn Sets of Coloured Petri Nets. In: Rozenberg, G. (ed.) Proceedings of ICATPN 1991, pp. 102–121 (1991)

    Google Scholar 

  39. Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)

    Google Scholar 

  40. Vardi, M., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: Proc. of IEEE Symposium on Logic in Computer Science, pp. 322–331 (1986)

    Google Scholar 

  41. Wolper, P., Leroy, D.: Reliable Hashing without Collision Detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200, Aarhus N, Denmark

    Lars Michael Kristensen & Thomas Mailund

Authors
  1. Lars Michael Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Mailund
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, National University of Singapore, Singapore

    Jin Song Dong

  2. University of York,  

    Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kristensen, L.M., Mailund, T. (2003). Efficient Path Finding with the Sweep-Line Method Using External Storage. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39893-6_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20461-9

  • Online ISBN: 978-3-540-39893-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation