Abstract
Abstraction is traditionally used in the process of verification. There, an abstraction of a concrete system is sound if properties of the abstract system also hold in the concrete system. Specifically, if an abstract state a satisfies a property ψ then all the concrete states that correspond to a satisfy ψ too. Since the ideal goal of proving a system correct involves many obstacles, the primary use of formal methods nowadays is falsification. There, as in testing, the goal is to detect errors, rather than to prove correctness. In the falsification setting, we can say that an abstraction is sound if errors of the abstract system exist also in the concrete system. Specifically, if an abstract state a violates a property ψ, then there exists a concrete state that corresponds to a and violates ψ too.
An abstraction that is sound for falsification need not be sound for verification. This suggests that existing frameworks for abstraction for verification may be too restrictive when used for falsification, and that a new framework is needed in order to take advantage of the weaker definition of soundness in the falsification setting.
We present such a framework, show that it is indeed stronger (than other abstraction frameworks designed for verification), demonstrate that it can be made even stronger by parameterizing its transitions by predicates, and describe how it can be used for falsification of branching-time and linear-time temporal properties, as well as for generating testing goals for a concrete system by reasoning about its abstraction.
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
Ball, T.: A theory of predicate-complete test coverage and generation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 1–22. Springer, Heidelberg (2005)
Benthem, J.: Languages in actions: categories, lambdas and dynamic logic. Studies in Logic 130 (1991)
Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. Computer Aided Verification, 274–287 (1999)
Bruns, G., Godefroid, P.: Model checking with 3-valued temporal logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004)
Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. Technical Report MSR-TR-2005-50, Microsoft Research (2005)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)
Dijksta, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dams, D., Namjoshi, K.S.: Automata as abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 216–232. Springer, Heidelberg (2005)
Fraer, R., Kamhi, G., Ziv, B., Vardi, M., Fix, L.: Prioritized traversal: efficient reachability analysis for verication and falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 389–402. Springer, Heidelberg (2000)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)
Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL, pp. 122–131 (2005)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Huth, M., Jagadeesan, R., Schmidt, D.: Model checking partial state spaces with 3-valued temporal logics. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1987)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design 19(3), 291–314 (2001)
Larsen, K.G., Thomsen, G.B.: A modal process logic. In: Proc. 3th Symp. on Logic in Computer Science, Edinburgh (1988)
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108–117 (1990)
Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted java programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 284–298. Springer, Heidelberg (2001)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1981)
Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)
Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)
Sipma, H.B.: Diagram-based Verification of Discrete, Real-time and Hybrid Systems. PhD thesis, Stanford University, Stanford, California (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ball, T., Kupferman, O., Yorsh, G. (2005). Abstraction for Falsification. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_8
Download citation
DOI: https://doi.org/10.1007/11513988_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)