Abstract
Partial order model-checking is an approach to reduce time and memory in model-checking concurrent programs. On-the-fly model-checking is a technique to eliminate part of the search by intersecting the (negation of the) checked property with the state space during its generation. We prove conditions under which these two methods can be combined in order to gain from both reductions. An extension of the model-checker SPIN, which implements this combination, is studied, showing substantial reduction over traditional search, not only in the number of reachable states, but directly in the amount of memory and time used.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
J. R. Büchi, On a decision method in restricted second order arithmetic, in E. Nagel et al. (eds.), Proceeding of the International Congress on Logic, Methodology and Philosophy of Science, Stanford, CA, Stanford University Press, 1960, 1–11.
C. Courcoubetis, M. Vardi, P. Wolper, M, Yanakakis, Memory-efficient algorithms for the verification of temporal properties, Formal methods in system design 1 (1992) 275–288.
J. C. Fernandez, L. Mounier, C. Jard, T. Jeron, On-the-fly verification of finite transition systems, Formal Methods in System Design 1 (1992), Kluwer, 251–273.
P. Godefroid, Using partial orders to improve automatic verification methods, Computer Aided Verification 1990, DIMACS, Vol 3, 1991, 321–339.
P. Godefroid, P. Wolper, A Partial Approach to Model Checking, 6th LICS, 1991, Amsterdam, 406–415.
G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall Software Series, 1992.
G. J. Holzmann, P. Godefroid, D. Pirottin, Coverage preserving reduction strategies for reachability analysis, Proc. IFIP, Symp. on Protocol Specification, Testing, and Verification, June 1992, Orlando, U.S.A., 349–364.
G. J. Holzmann, D. Peled, STREM: A static reduction method, Manuscript, 1994, available from the authors.
S. Katz, D. Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing 6 (1992), 107–120.
S. Katz, D. Peled, Defining conditional independence using collapses, Theoretical Computer Science 101 (1992), 337–359, a preliminary version appeared in BCS-FACS Workshop on Semantics for Concurrency, Leicester, England, July 1990, Springer, 262–280.
R. P. Kurshan, Reducibility in analysis of coordination, Lecture Notes in Communication and Information, Springer, 103, 19–39.
M. Z. Kwiatkowska, Fairness for non-interleaving concurrency, Phd. Thesis, Faculty of Science, University of Leicester, 1989.
L. Lamport, What good is temporal logic, IFIP Congress, North Holland, 1983, 657–668.
O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, 11 th ACM POPL, 1984, 97–107.
A. Mazurkiewicz, Trace semantics, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 279–324.
D, Peled, All from one, one for all, on model-checking using representatives, 5 th international conference on Computer Aided Verification, Greece, 1993, LNCS, Springer, 409–423.
A. Valmari, Stubborn sets for reduced state space generation, 10th International Conference on Application and Theory of Petri Nets, Vol. 2, 1–22, Bonn, 1989.
A. Valmari, A Stubborn attack on state explosion, in E.M. Clarke, R.P. Kurshan (eds.), CAV'90, DIMACS, Vol 3, 1991, 25–42.
A. Valmari, On-The-Fly Verification of stubborn sets, 5th CAV, Greece, 1993, LNCS 697, Springer, 397–408.
P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, Proceedings of 24th IEEE symposium on foundation of computer science, Tuscan, 1983, 185–194.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peled, D. (1994). Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_69
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_69
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive