Abstract
A common approach for verifying a concurrent system is to compute the product of finite-state descriptions of the processes involved. Unfortunately, the size of this product is frequently prohibitive due, among other causes, to the modelling of concurrency by interleaving. However, computing all interleavings of concurrent events is not a priori necessary for verification: interleavings corresponding to the same concurrent execution contain related information. One can thus hope to be able to verify properties of a concurrent system without computing all interleavings of its executions. This paper overviews a collection of techniques that make this possible.
This work was supported by the Esprit BRA action REACT (6021) and by the Belgian Incentive Program “Information Technology” — Computer Science of the future, initiated by the Belgian State — Prime Minister's Office — Science Policy Office. The scientific responsibility is assumed by its authors.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117–126, 1987.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
P. Godefroid, G. J. Holzmann, and D. Pirottin. State space caching revisited. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 176–185, Rutgers, June 1990. Springer-Verlag.
P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proc. 6th Symp. on Logic in Computer Science, pages 406–415, Amsterdam, July 1991.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 332–342, Aalborg, July 1991. Springer-Verlag.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149–164, April 1993.
G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337–359, 1992.
A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, volume 255 of Lecture Notes in Computer Science, pages 279–324, 1986.
K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
W. T. Overman. Verification of Concurrent Systems: Function and Timing. PhD thesis, University of California Los Angeles, 1981.
D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
D. K. Probst and H. F. Li. Abstract specification, composition and proof of correctness of delay-insensitive circuits and systems. Cs-vlsi-88-2, Department of Computer Science, Concordia University, Montreal, Quebec Canada, 1989.
D. K. Probst and H. F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 146–155, Rutgers, June 1990. Springer-Verlag.
A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156–165, Rutgers, June 1990. Springer-Verlag.
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990, volume 483 of Lecture Notes in Computer Science, pages 491–515. Springer-Verlag, 1991.
A. Valmari. On-the-fly verification with stubborn sets. In Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75–123. Lecture Notes in Computer Science, Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wolper, P., Godefroid, P. (1993). Partial-order methods for temporal verification. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_17
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive