Abstract
We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification in a novel way. In particular, it allows and shows how to use the set of reachable states of the abstract system in a deductive proof even when the abstract model does not satisfy the specification and when it simulates the concrete system with respect to a weaker simulation notion than Milner’s.
This work has been partly performed while the first two authors were visiting the Computer Science Laboratory, SRI International. Their visits were funded by NSF Grants No. CCR-9712383 and CCR-9509931.
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
F. Balarin and A.L. Sangiovanni-Vincentelli. Am iterative approach to language containment. In Costas Courcoubetis, editor, Computer Aided Verification: 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 29–40. Springer-Verlag, 1993.
K.A. Barlett, R.A. Scantlebury, and P.T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5), 1969.
K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In S. Graf and M. Schwartzbach, editors, TACAS’00, volume 1785 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
K. Baukus, Y. Lakhnech, and K. Stahl. Verifying universal properties of parameterized networks. In M. Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of Lecture Notes in Computer Science, pages 291–304. Springer-Verlag, 2000.
S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Formal Methods in System Design, 1999. To appear.
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems automatically and compositionally. In Alan J. Hu and Moshe Y. vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 319–331. Springer-Verlag, 1998.
S. Bensalem, Y. Lakhnech, and S. Owre. Invest: A tool for the verification of invariants. In Alan J. Hu and Moshe Y. vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 505–510. Springer-Verlag, 1998.
A. Bouajjani, J. Cl. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification. Rutgers-American Mathematical Society, Association for Computing Machinery, June 1990.
Ahmed Bouajjani, Yassine Lakhnech, and Sergio Yovine. Model checking for extended timed temporal logics. In B. Jonsson and J. Parrow, editors, 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT’96, volume 1135 of Lecture Notes in Computer Science, pages 306–326. Springer-Verlag, 1996.
Bettina Buth, Karl-Heinz Buth, Martin Fräanzle, Burghard v. Karger, Yassine Lakhnech, Hans Langmaack, and Markus Müuller-Olm. Provably correct compiler development and implementation. Compiler Construction, 1992.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, Lecture Notes in Computer Science, pages 154–169. Springer-Verlag, 2000.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994.
R. Cleaveland, P. Iyer, and D. Yankelevitch. Optimality in abstractions of model checking. In A Mycroft, editor, Static Analysis, volume 983 of Lecture Notes in Computer Science, pages 51–63, 1995.
M. A. Colon and T. E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. Lecture Notes in Computer Science, 1427:293–304, 1998.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM symp. of Prog. Lang., pages 238–252. ACM Press, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th ACM POPL, pages 269–282, 1979.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, 1997.
F.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large packets. In A case study in computer checked verification, Logic Group Preprint Series 100. Utrecht University, 1993.
K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe, FME’96 Symposium, volume 1051 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-R9420, Centrum voor Wiskunde en Informatica (CWI), March 1994.
M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In 36th Annual Symposium on Foundations of Computer Science (FOCS’95), pages 453–462, Los Alamitos, October 1995. IEEE Computer Society Press.
Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, To appear, 2000.
R.P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press, 1994.
David Lee and Mihalis Yannakakis. Online minimization of transition systems (extended abstract). In Proceedings of the Twenty-Fourth Annual ACM Symposium on the Theory of Computing, pages 264–274, Victoria, British Columbia, Canada, 4–6 May 1992.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
S. Mauw and G.J. Veltink editors. Algebraic Specification of Communication Protocols. Number 36 in Cambridge Tracts in Theoretical Computer Science. 1993.
S.S. Muchnick and N. D. Jones, editors. Program Flow Analysis. Prentice-Hall, 1981.
K. S. Namjoshi and R. P. Kurshan. Syntactic program transformations for automatic abstraction. In Computer Aided Verification, Lecture Notes in Computer Science, pages 435–449. Springer-Verlag, 2000.
H. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In R. Alur and T.A. Henzinger, editors, 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 208–219. Springer-Verlag, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S. (2001). Incremental Verification by Abstraction. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_8
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive