Abstract
We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of states in an abstraction of this graph, which is repeatedly refined in the search for a counterexample computation, ruling out large portions of the graph before they are expanded to the state-level. This can lead to large savings, even in the case of finite-state systems. Only local conditions need to be checked at each step, and previously proven properties can be used to further constrain the search. Although the resulting method is not always automatic, it provides a flexible and general framework that can be used to integrate a diverse number of other verification tools.
This research was supported in part by the National Science Foundation under grant CCR-92-23226, the Advanced Research Projects Agency under NASA grant NAG2-892, the United States Air Force Office of Scientific Research under grant F49620-93-1-0139, the Department of the Army under grant DAAH04-95-1-0317, and a gift from Intel Corporation.
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
Bhat, G., Cleaveland, R., and Grumberg, O. Efficient on-the-fly model checking for CTL*. In Proc. 10th IEEE Symp. Logic in Comp. Sci. (1995), pp. 388–397.
BJørner, N., Browne, A., Chang, E., Colón, M., Kapur, A., Manna, Z., Sipma, H., and Uribe, T. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Proc. 8th Intl. Conference on Computer Aided Verification (July 1996), Springer-Verlag.
Bjørner, N., Browne, A., and Manna, Z. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming (Sept. 1995), vol. 976 of LNCS, Springer-Verlag, pp. 589–623.
Bouajjani, A., Fernandez, J.-C., and Halbwachs, N. Minimal model generation. In Proc. 2nd Intl. Conference on Computer Aided Verification (1990), vol. 531 of LNCS, pp. 197–203.
Bradfield, J. C. Verifying Temporal Properties of Systems. Birkhäuser, 1992.
Browne, A., Manna, Z., and Sipma, H. Generalized verification diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science (Dec. 1995), vol. 1026 of LNCS, pp. 484–498.
Bryant, R. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35, 8 (Aug. 1986), 677–691.
Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE Symp. Logic in Comp. Sci. (1990), IEEE Computer Society Press, pp. 428–439.
Chandra, A., Iyengar, V., Jawalekar, R., Mullen, M., Nair, I., and Rosen, B. Architectural verification of processors using symbolic instruction graphs. In International Conference on Computer Design: VLSI in Computers and Processors (1994), IEEE Press, pp. 454–459.
Clarke, E., and Emerson, E. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. IBM Workshop on Logics of Programs (1981), vol. 131 of LNCS, Springer-Verlag, pp. 52–71.
Fix, L., and Grumberg, O. Verification of temporal properties. J. Logic and Computation 6, 3 (1996), 343–362.
Jaffar, J., and Lassez, J.-L. Constraint logic programming. In Proc. 14th ACM Symp. Princ. of Prog. Lang. (Jan. 1987), pp. 111–119.
Manna, Z., and Pnueli, A. Temporal verification diagrams. In Proc. Int. Symp. on Theoretical Aspects of Computer Software (1994), vol. 789 of LNCS, Springer-Verlag, pp. 726–765.
Manna, Z., and Pnueli, A.Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
McMillan, K. L. Symbolic Model Checking. Kluwer Academic Pub., 1993.
Queille, J., and Sifakis, J. Specification and verification of concurrent systems in CESAR. In Intl. Symposium on Programming (1982), M. Dezani-Ciancaglini and U. Montanari, Eds., vol. 137 of LNCS, Springer-Verlag, pp. 337–351.
Saraswat, V. A. Concurrent Constraint Programming. MIT Press, 1993.
Sokolsky, O. V., and Smolka, S. A. Local model checking for real-time systems. In Proc. 7th Intl. Conference on Computer Aided Verification (1995), vol. 939 of LNCS, pp. 211–224.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sipma, H.B., Uribe, T.E., Manna, Z. (1996). Deductive model checking. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_70
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_70
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive