Advertisement

A Compositional Sweep-Line State Space Exploration Method

  • Lars Michael Kristensen
  • Thomas Mailund
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)

Abstract

State space exploration is a main approach to verification of finite-state systems. The sweep-line method exploits a certain kind of progress present in many systems to reduce peak memory usage during state space exploration. We present a new sweep-line algorithm for a compositional setting where systems are composed of subsystems. The compositional setting makes it possible to divide subsystem progress measures into monotone and non-monotone progress measures to further reduce peak memory usage. We show that in a compositional setting, it is possible to automatically obtain a progress measure for the system by combining the progress measure for each subsystem to a progress measure for the full system.

References

  1. 1.
    S. Christensen, L.M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Proc. of TACAS’01, volume 2031 of LNCS, pages 450–464. Springer-Verlag, 2001.Google Scholar
  2. 2.
    E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetries in Temporal Logic Model Checking. In Proc. of CAV’93, pages 450–462. Springer-Verlag, 1993.Google Scholar
  3. 3.
    P. Godefroid, G.J. Holzman, and D. Pirottin. State Space Caching Revisited. In Proc. of CAV’92, volume 663 of LNCS, pages 178–191. Springer-Verlag, 1992.Google Scholar
  4. 4.
    S. Gordon, L.M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol. In Proc. of ICATPN’02, volume 2360 of LNCS, pages 182–202. Springer-Verlag, 2002.Google Scholar
  5. 5.
    C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  6. 6.
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.Google Scholar
  7. 7.
    C. Jard and T. Jeron. Bounded-memory Algorithms for Verification On-the-fly. In Proc. of CAV’91, volume 575 of LNCS, pages 192–202. Springer-Verlag, 1991.Google Scholar
  8. 8.
    L.M. Kristensen and T. Mailund. A Compositional Sweep-Line State Space Exploration Method. Technical report, Department of Computer Science, University of Aarhus, 2002. Available via: http://www.daimi.au.dk/~mailund/ps/lmktm_compo.ps.
  9. 9.
    L.M. Kristensen and T. Mailund. A Generalised Sweep-Line Method for Safety Properties. In Proc. of FME’02, volume 2391 of LNCS, pages 549–567. Springer-Verlag, 2002.Google Scholar
  10. 10.
    K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer, 1(1+2):134–152, October 1997.zbMATHGoogle Scholar
  11. 11.
    T. Mailund. SweepChecker. http://sweepchecker.sourceforge.net.
  12. 12.
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  13. 13.
    R. Milner. Communication and Concurrency. Prentice-Hall International Series in Computer Science. Prentice-Hall, 1989.Google Scholar
  14. 14.
    D. Peled. All from One, One for All: On Model Checking Using Representatives. In Proc. of CAV’93, volume 697 of LNCS, pages 409–423. Springer-Verlag, 1993.Google Scholar
  15. 15.
    R. Tarjan. Depth-First Search and Linear Graph Algorithms. SIAM Journal of Computing, 1(2):146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    A. Valmari. Stubborn Sets for Reduced State Space Generation. In Advances in Petri Nets’ 90, volume 483 of LNCS, pages 491–515. Springer-Verlag, 1990.Google Scholar
  17. 17.
    A. Valmari. Compositionality in State Space Verification Methods. In Proc. of ICATPN’96, volume 1091 of LNCS, pages 29–56. Springer-Verlag, 1996.Google Scholar
  18. 18.
    M. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verifcation. In Proc. of IEEE Symposium on Logic in Computer Science, pages 322–331, 1986.Google Scholar
  19. 19.
    P. Wolper and P. Godefroid. Partial Order Methods for Temporal Verification. In Proc. of CONCUR’93, volume 715 of LNCS, pages 233–246. Springer-Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Lars Michael Kristensen
    • 1
    • 2
  • Thomas Mailund
    • 2
  1. 1.School of Electrical and Information EngineeringUniversity of South AustraliaMawson Lakes Campus, Mawson LakesAUSTRALIA
  2. 2.Department of Computer ScienceUniversity of AarhusAarhus NDENMARK

Personalised recommendations