Advertisement

Search-Order Independent State Caching

  • Sami Evangelista
  • Lars Michael Kristensen
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6550)

Abstract

State caching is a memory reduction technique used by model checkers to alleviate the state explosion problem. It has traditionally been coupled with a depth-first search to ensure termination. We propose and experimentally evaluate an extension of the state caching method for general state exploring algorithms that are independent of the search order (i.e., search algorithms that partition the state space into closed (visited) states, open (to visit) states and unmet states).

Keywords

State Space Model Check Search Tree Cache Size Progress Measure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bao, T., Jones, M.: Time-Efficient Model Checking with Magnetic Disk. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 526–540. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P.: DiVinE – A Tool for Distributed Verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 278–281. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Behrmann, G., Larsen, K.G., Pelánek, R.: To Store or Not to Store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 433–445. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Bošnački, D., Elkind, E., Genest, B., Peled, D.: On Commutativity Based Edge Lean Search. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 158–170. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Bošnački, D., Leue, S., Lafuente, A.L.: Partial-Order Reduction for General State Exploring Algorithms. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 271–287. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
  8. 8.
    Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed Explicit-State Model Checking in the Validation of Communication Protocols. STTT 5, 247–267 (2004)CrossRefzbMATHGoogle Scholar
  9. 9.
    Evangelista, S., Kristensen, L.M.: Search-Order Independent State Caching. Technical report (2009), http://daimi.au.dk/~evangeli/doc/caching.pdf
  10. 10.
    Evangelista, S., Pradat-Peyre, J.-F.: Memory Efficient State Space Storage in Explicit Software Model Checking. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 43–57. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Geldenhuys, J.: State Caching Reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  13. 13.
    Godefroid, P., Holzmann, G.J., Pirottin, D.: State-Space Caching Revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 178–191. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  14. 14.
    Holzmann, G.J.: Tracing Protocols. AT&T Technical J. 64(10), 2413–2434 (1985)CrossRefGoogle Scholar
  15. 15.
    Holzmann, G.J.: Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching. IEEE Trans. Software Eng. 13(6), 683–696 (1987)CrossRefGoogle Scholar
  16. 16.
    Holzmann, G.J.: State Compression in Spin: Recursive Indexing and Compression Training Runs. In: SPIN 1997 (1997)Google Scholar
  17. 17.
    Jard, C., Jéron, T.: On-Line Model Checking for Finite Linear Temporal Logic Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 189–196. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  18. 18.
    Jard, C., Jéron, 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)CrossRefGoogle Scholar
  19. 19.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets — Modeling and Validation of Concurrent Systems. Springer, Heidelberg (2009)CrossRefzbMATHGoogle Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    Mateescu, R., Wijs, A.: Hierarchical Adaptive State Space Caching Based on Level Sampling. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 215–229. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Pelánek, R., Rosecký, V., Sedenka, J.: Evaluation of State Caching and State Compression Techniques. Technical report, Masaryk University, Brno (2008)Google Scholar
  24. 24.
    Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  25. 25.
    Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting Transition Locality in Automatic Verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 259–274. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Westergaard, M., Evangelista, S., Kristensen, L.M.: ASAP: An Extensible Platform for State Space Analysis. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 303–312. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  27. 27.
    Westergaard, M., Kristensen, L.M., Brodal, G.S., Arge, L.: The ComBack Method – Extending Hash Compaction with Backtracking. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 445–464. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Sami Evangelista
    • 1
    • 2
  • Lars Michael Kristensen
    • 3
  1. 1.Computer Science DepartmentAarhus UniversityDenmark
  2. 2.LIPNUniversité Paris 13France
  3. 3.Department of Computer EngineeringBergen University CollegeNorway

Personalised recommendations