Abstract
We present a method for computing abstractions of infinite state systems compositionally and automatically. Given a concrete system S = S 1 ∥ ... ∥ S n of programs and given an abstraction function α, using our method one can compute an abstract system S a = S a1 ∥ ... ∥ S a n such that S simulates S a. A distinguishing feature of our method is that it does not produce a single abstract state graph but rather preserves the structure of the concrete system. This feature is a prerequisite to benefit from the techniques developed in the context of model-checking for mitigating the state explosion. Moreover, our method has the advantage that the process of constructing the abstract system does not depend on whether the computation model is synchronous or asynchronous.
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
References
S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Accepted in Formal Methods in System Design. To appear.
N. Bjørner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1), 1997.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994.
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.
D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven, 1996.
D. Dams, R. Gerth, G. Döhmen, R. Herrmann, P. Kelb, and H. Pargmann. Model checking using adaptive state and data abstraction. In CAV'94, volume 818 of LNCS. Springer-Verlag, 1994.
D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In CAV'93, volume 697 of LNCS. Springer-Verlag, 1993.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL, ECTL and CTL In ROCOMET'94. IFIP Transactions, North-Holland/Elsevier, 1994.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions in Programming Languages and Systems, 19(2), 1997.
J. Dingel and Th. Filkorn. Model checking for infinite state systems using data abstraction. In CAV'95, volume 939 of LNCS, pages 54–69. Springer-Verlag, 1995.
S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Accepted to Distributed Computing, 1995.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV'93, volume 697 of LNCS. Springer-Verlag, 1993.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV'97, volume 1254 of LNCS, 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 FME'96, volume 1051 of LNCS. Springer-verlag, 1996.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-119420, CWI, March 1994.
P. Kelb. Abstraktionstechniken für Automatische Verifikationsmethoden. PhD thesis, University of Oldenburg, 1995.
R.P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. 1994.
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.
D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993.
Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):97–130, 1991.
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.
K.L. McMillan. Symbolic model checking. Kluwer Academic Publ., Boston, 1993.
O. Müller and T. Nipkow.Combining model checking and deduction for I/O-utomata. In TACAS'95, volume 1019 of LNCS, 1995.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 1995.
J. X. Su, D. L. Dill, and C. Barrett. Automatic generation of invariants in processor verification. In FMCAD '96, volume 1166 of LNCS, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bensalem, S., Lakhnech, Y., Owre, S. (1998). Computing abstractions of infinite state systems compositionally and automatically. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028755
Download citation
DOI: https://doi.org/10.1007/BFb0028755
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive
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.