Abstract
The purpose of this paper is to verify a distributed cache memory system by using the following general verification method: verify the properties characterizing a complex system on some small finite abstraction of it, obtained as a composition of abstractions of each component of the system. For a large class of systems including infinite state systems, the abstractions of the components can be obtained by replacing all operators on concrete domains by abstract operators on some abstract domain. This holds also for the abstraction of the control part of the system as we consider a kind of guarded command programs where all the control is expressed in terms of operations on explicit control variables.
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.
This work was partially supported by ESPRIT Basic Research Action “REACT”.
Verimag is a joint laboratory of CNRS, Institut National Polytechnique de Grenoble, Universitée J. Fourier and Verilog SA associated with IMAG.
Download to read the full chapter text
Chapter PDF
References
Y. Afek, G. Brown, and M. Meritt. Lazy caching. ACM Transactions on Programming Languages and Systems, 15(1), 1993.
P. and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.
E. Clarke, O. Grumberg, D. Long. Model checking and abstraction. In POPL, 1991.
J. Davis, R. Gerth, W. Jannsen, B. Jonsson, S. Katz, G. Lowe, A. Pnueli, and C. Rump. Verifying sequentially consistent memory. Preliminary report, 1993.
E. A. Emerson and J. Y. Halpern. 'sometimes’ and ‘not never’ revisited: On branching versus linear time. In POPL, 1983. also in Journal of ACM, 33:151–178.
S. Graf and C. Loiseaux. Program verification using compositional abstraction. In TAPSOFT 93, joint conference CAAP/FASE. LNCS 668, Springer Verlag, April 1993.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV, Heraklion Crete. LNCS 697, Springer Verlag, 1993.
B. Jonsson, A. Pnueli, and C. Rump. Proving refinement using transduction. Technical report, Weizmann Institute, 1993.
R.P. Kurshan. Analysis of discrete event coordination. In REX Workshop on Stepwise Refinement of Distributed Systems, Mook. LNCS 430, Springer Verlag, 1989.
L. Lamport. How to make a multiprocessor that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28:690–691, 1979.
L. Lamport. The temporal logic of actions. Technical Report 79, DEC Systems Research Center, 1991.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. To appear in Formal Methods in System Design, also in CAV'92.
C. Loiseaux. Vérification symbolique de programmes réactifs à l'aide d'abstractions. Thesis, Verimag, Grenoble, January 1994.
D. E. Long. Model checking, abstraction and compositional verification. Phd thesis, Carnegie Mellon University, July 1993.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models for Concurrent Systems. NATO, ASI Series F, Vol.13, 1985.
A. Pnueli. Specification and Development of reactive Systems. In Conference IFIP, Dublin. North-Holland, 1986.
G. Shurek and O. Grumberg. The modular framework of computer-aided verification: motivation, solutions and evaluation criteria. In CAV, LNCS 531, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, S. (1994). Verification of a distributed cache memory by using abstractions. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_55
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_55
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive