Abstract
The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parameterized) process networks.
The main contributions of the paper are a formulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, verifying the correctness of the Futurebus+ design for all singlebus configurations, extending the technique to tree architectures, and establishing that the presented method is a precise dual to the top-down invariant generation method used in deductive verification.
This research was supported in part by a gift from Intel, and an Infrastructure grant from the Israeli Ministry of Science and the Arts.
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
K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.
N. Bjørner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In LNCS 976, 1995.
R.V. Book and F. Otto. String-Rewriting Systems, Springer, 1993.
A. Bouajjani and O. Maler, Reachability Analysis of Push-down Automata. Workshop on Infinite-state Systems, Pisa, 1996.
M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In PODC'86.
J.R. Burch, E.M. Clarke, et al. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
D.A. Basin and N. Klarlund. Hardware verification using 2nd-order logic. In P. Wolper, editor, CAV'95, LNCS 939, 1995.
S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. CAV'96, 1996.
R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(12):1035–1044, 1986.
E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. Logics of Programs, LNCS 131, 1981.
E.M. Clarke, et al. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Sys., 1986.
E.M. Clarke, O. Grumberg, et al. Verification of the futurebus+ cache coherence protocol. Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. 1993.
E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR'95, 1995.
J. Doner. Tree Acceptors and some of their applications, JCSS 4, 1970.
E. A. Emerson, K. S. Namjoshi. Reasoning about rings. POPL'95, 1995.
E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, CAV'96, 1996.
F. Gecseg and M. Steinby. Tree Automata Akademiai Kiado, 1984.
N. Halbwachs, F. Lagnier, et al. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6/7), 1992.
J.G. Henriksen, J. Jensen, et al. Mona: Monadic second-order logic in practice. In TACAS '95, LNCS 1019, 1996.
C.N. Ip and D. Dill. Verifying systems with replicated components in Munϕ. In R. Alur and T. Henzinger, editors, CAV'96, 1996.
O. Kupferman and O. Grumberg. Branching Time Temporal Logic and Amorphous Tree Automata. Information and Computation 125, 1996.
R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In P. Rudnicki, editor, PODC'89, Edmonton, AB, Canada, 1989.
D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL'97, Paris, 1997.
Z. Manna, A. Anuchitanukul, et al. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Stanford University, 1994.
K.L McMillan. Symbolic Model Checking. 1993.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, CAV'96, 1996.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. International Symposium on Programming,LNCS 137, 1982.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In LNCS 407, 1989.
A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675–735, 1992.
N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, SRI International, Menlo Park, CA, 1993.
J.W. Thatcher, J.B. Wright. Generalized finite automata with application to a decision procedure in second order logic. Math. Sys. Theory 2, 1968.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In LNCS 407, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Resten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E. (1997). Symbolic model checking with rich assertional languages. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_41
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive