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.
Supported by an Australian Research Council (ARC) Discovery Grant (DP02105).
Supported by the Danish Natural Science Research Council.
Chapter PDF
Similar content being viewed by others
References
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.
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.
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.
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.
C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
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.
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.
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.
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.
T. Mailund. SweepChecker. http://sweepchecker.sourceforge.net.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
R. Milner. Communication and Concurrency. Prentice-Hall International Series in Computer Science. Prentice-Hall, 1989.
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.
R. Tarjan. Depth-First Search and Linear Graph Algorithms. SIAM Journal of Computing, 1(2):146–160, 1972.
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.
A. Valmari. Compositionality in State Space Verification Methods. In Proc. of ICATPN’96, volume 1091 of LNCS, pages 29–56. Springer-Verlag, 1996.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michael Kristensen, L., Mailund, T. (2002). A Compositional Sweep-Line State Space Exploration Method. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_21
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive