Abstract
Practicing verifiers of finite-state concurrent systems should be able to adapt our partial-order methods for verifying delay-insensitive systems to other verification problems. We answer the question, is it possible to control state explosion arising from various sources during automatic verification (model checking) of delay-insensitive systems? State explosion due to concurrency is handled by introducing a partial-order representation for processes, and defining system correctness as a simple relation between two partial orders on the same set of system events. State explosion due to nondeterminism is handled when the system to be verified has a compact, finite recurrence structure. Backwards branching through representations is a further optimization. In system verification, we start with models of system components that explicitly distinguish concurrency, choice and recurrence structure; during model checking, this a priori structure of components allows us to construct a compact, finite representation of the specification-constrained implementation — without prior composition of system components. The fully-implemented POM verification system has polynomial space and time performance on traditional asynchronous-circuit benchmarks that are exponential in space and time for other verification systems; in general, the cost of running our verification algorithm is proportional to the size of the constructed system representation.
This research was supported by the Natural Sciences and Engineering Research Council of Canada under grants A3363, A0921 and MEF0040121.
Chapter PDF
Similar content being viewed by others
Keywords
References
D.L. Black, “On the existence of delay-insensitive fair arbiters”, Distributed Computing, Vol. 1, No. 4, October 1986, pp. 205–225.
D.L. Dill, “Trace theory for automatic hierarchical verification of speed-independent circuits”, Ph. D. Thesis, Department of Computer Science, Carnegie Mellon University, Report CMU-CS-88-119, February 1988. Also MIT Press, 1989.
A.J. Martin, “Compiling communicating processes into delay-insensitive VLSI circuits”, Distributed Computing, Vol. 1, No. 4, October 1986, pp. 226–234.
V.R. Pratt, “Modelling concurrency with partial orders”, Int. J. of Parallel Prog., Vol. 15, No. 1, February 1986, pp. 33–71.
V.R. Pratt, “Modelling concurrency with geometry”, Proc. 18th Ann. ACM Symposium on Principles of Programming Languages, January 1991, pp. 311–322.
D.K. Probst and H.F. Li, “Abstract specification of synchronous data types for VLSI and proving the correctness of systolic network implementations”, IEEE Trans. on Computers, Vol. C-37, No. 6, June 1988, pp. 710–720.
D.K. Probst and H.F. Li, “Abstract specification, composition and proof of correctness of delay-insensitive circuits and systems”, Technical Report, Department of Computer Science, Concordia University, CS-VLSI-88-2, April 1988 (Revised March 1989).
D.K. Probst and H.F. Li, “Partial-order model checking of delay-insensitive systems”. In R. Hobson et al. (Eds.), Canadian Conference on VLSI 1989, Proceedings, Vancouver, BC, October 1989, pp. 73–80.
D.K. Probst and H.F. Li, “Using partial-order semantics to avoid the state explosion problem in asynchronous systems”. In E.M. Clarke and R.P. Kurshan, (Eds.), Workshop on Computer-Aided Verification '90, June 1990, DIMACS Series, Vol. 3, 1991, pp. 15–24. Also Lect. Notes in Comput. Sci., Springer Verlag, forthcoming.
D.K. Probst and H.F. Li, “Modelling reactive processes using partial orders”. In M. Kwiatkowska et al. (Eds.), Semantics for Concurrency, Leicester 1990, Leicester, UK, July 1990, Workshops in Computing, Springer Verlag, 1990, pp. 324–343.
D.K. Probst and L.C. Jensen, “Controlling state explosion during automatic verification of delay-insensitive and delay-constrained VLSI systems using the POM verifier”. In S. Whitaker, (Ed.), Third NASA Symposium on VLSI Design, Moscow, ID, October 1991, Proceedings, pp. 8.2.1–8.2.8.
J.v.d. Snepscheut, “Trace theory and VLSI design”, Lect. Notes in Comput. Sci. 200, Springer Verlag, 1985.
J.T. Udding, “A formal model for defining and classifying delay-insensitive circuits”, Distributed Computing, Vol. 1, No. 4, October 1986, pp. 197–204.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Probst, D.K., Li, H.F. (1992). Partial-order model checking: A guide for the perplexed. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_31
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive