Abstract
The combination of abstraction and state exploration techniques is the most promising recipe for a successful verification of properties of large or infinite state systems. In this work, we present a general, yet effective, algorithm for computing automatically boolean abstractions of infinite state systems, using decision procedures. The advantage of our approach is that it is not limited to particular concrete domains, but can handle different kinds of infinite state systems. Furthermore, our approach provides, through the use of model checking as a tool for the exploration of the state-space of the abstract system, an automatic way of refining the abstraction until the property of interest is verified or a counterexample is exhibited. We illustrate our approach on some examples and discuss its implementation.
This research was supported by DARPA contract F30602-97-C-0040.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Bensalem, S., Lakhnech, Y., Saïdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 323–335. Springer, Heidelberg (1996)
Bjorner, N., Browne, A., Manna, Z.: Automatic Generation of Invariants and Intermediate Assertions. Theoretical Computer Science (1997)
Mani Chandy, K., Misra, J.: Parallel Program Design. Addison-Wesley, Reading (1988)
Chou, C.-T.: Simple proof techniques for property preservation via simulation. Information Processing Letters 60(3), 129–134 (1996)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Colon, M., Uribe, T.: Generating finite-state abstractions of reactive systems using decision procedures. In: CAV 1998. LNCS, Springer, Heidelberg (1998)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL (January 1977)
Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven (July 1996)
Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In: Olderog, E.-R. (ed.) IFIP Conference PROCOMET 1994, pp. 561–581 (1994)
Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)
Dingel, J., Filkorn, T.: Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)
Graf, S.: Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distributed Computing (1995)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. Technical report, Department of Philosophy (October 1993)
Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)
Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. Technical report, Department of Philosophy, Utrech University, The Netherlands (March 1994)
Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39–50. Springer, Heidelberg (1999)
Kurshan, R.P.: Computer-aided verification of coordinating processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press (1994)
Lesens, D., Saïdi, H.: Automatic verification of parameterized networks of processes by abstraction. In: Moller, F. (ed.) 2nd International Workshop on Verification of Infinite State Systems: Infinity 1997, Bologna, Italy, July 1997. Electronic Notes in Theoretical Computer Science, vol. 9, Elsevier, Amsterdam (1997)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6(1) (January 1995)
Manna, Z., Pnueli, A.: The Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
Owre, S., Shankar, N., Rushby, J.M.: A tutorial on specification and verification using pvs. Technical report, Computer Science Laboratory, SRI International (February 1993)
Saïdi, H.: Modular and incremental analysis of concurrent software systems. In: 14th IEEE International Conference on Automated Software Engineering, Cocoa Beach, FL, pp. 92–101. IEEE Computer Society Press, Los Alamitos (1999)
Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Saïdi, H. (2000). Model Checking Guided Abstraction and Analysis. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-45099-3_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67668-3
Online ISBN: 978-3-540-45099-3
eBook Packages: Springer Book Archive