Abstract
Data-independent systems are an important class of infinite-state systems which can be subject to model checking by first building finite-state property-preserving abstractions. Exploiting data independence in practice involves user guidance, either in terms of the abstraction itself or in terms of symmetry properties of the system. In this paper we present a constraint-based verification technique that automatically handles data-independent systems. Our technique introduces a unified, automata-based model for infinite-state systems and LTL formulas. The technique can be seen as a generalization of explicit state model checker for reachability and LTL properties. We have implemented our technique using logic programming with tabulation and constraints. We also describe an extension to the automata model that permits verification of a richer class of systems. We show its power by analyzing configuration (security) vulnerabilities in a computer system.
This research was supported in part by NSF grants EIA-9705998, CCR-9876242, IIS-0072927, CCR-0205376, CCR-0311512, and ONR grant N000140110967.
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
Aggarwal, S., Kurshan, R.P., Sabnani, K.: A calculus for protocol specification and validation. Protocol Specification, Testing and Verification, III (1983)
Basu, S., Narayan Kumar, K., Pokorny, L.R., Ramakrishnan, C.R.: Resourceconstrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 236. Springer, Heidelberg (2002)
Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.M.: Local and symbolic bisimulation using tabled constraint logic programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, p. 166. Springer, Heidelberg (2001)
Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Chan, W., Anderson, R.J., Beame, P., Notkin, D.: Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 223. Springer, Heidelberg (1999)
Du, X., Ramakrishnan, C.R., Smolka, S.A.: Tabled resolution + constraints: A recipe for model checking real-time systems. In: RTTS (2000)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138, 353–389 (1995)
Norris Ip, C., Dill, D.L.: Better verification through symmetry. FMSD (1996)
Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: POPL (1987)
Jonsson, B., Parrow, J.: Deciding bisimulation equivalences for a class of nonfinite- state programs. Information and Computation 107(2) (December 1993)
Lazić, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University (1999)
Lin, H.: Symbolic transition graphs with assignments. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
Lin, H.: Model checking value-passing processes. In: APSEC (2001)
Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1984)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)
Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstractions. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Pemmasani, G., Ramakrishnan, C.R., Ramakrishnan, I.V.: Efficient model checking of real time systems using tabled logic programming and constraints. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, p. 100. Springer, Heidelberg (2002)
Pnueli, A., Kesten, Y., Vardi, M.: Yes, Matilda! Abstraction can Replace Deduction, even for Computational Models which are BAD (Buchi Automata with Data). In: VHS Meeting, Grenoble (1999)
Robert Pokorny, L., Ramakrishnan, C.R.: Model checking linear temporal logic using tabled logic programming. In: TAPD (2000)
Ramakrishnan, C.R., Sekar, R.: Model-based analysis of configuration vulnerabilities. Journal of Computer Security (JCS) 10(1 / 2), 189–209 (2002)
Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., et al.: XMC: A logicprogramming- based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Rodeh, Y., Shtrichman, O.: Finite instantiations in equivalence logic with uninterpreted functions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 144. Springer, Heidelberg (2001)
Roychoudhury, A., Ramakrishnan, C.R., Ramakrishnan, I.V.: Justifying proofs using memo tables. In: PPDP (2000)
Tamaki, H., Sato, T.: OLDT resolution with tabulation. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225. Springer, Heidelberg (1986)
Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL (1986)
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the picalculus: Model checking mobile processes using tabled resolution. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 116–131. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sarna-Starosta, B., Ramakrishnan, C.R. (2003). Constraint-Based Model Checking of Data-Independent Systems. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-39893-6_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20461-9
Online ISBN: 978-3-540-39893-6
eBook Packages: Springer Book Archive