Abstract
The construction of abstractions is essential for reducing large or infinite state systems to small or finite state systems. Boolean abstractions, where boolean variables replace concrete predicates, are an important class that subsume several abstraction schemes. We show how boolean abstractions can be constructed simply, efficiently, and precisely for infinite state systems while preserving properties in the full µ-calculus. We also propose an automatic refinement algorithm which refines the abstraction until the property is verified or a counterexample is found. Our algorithm is implemented as a proof rule in the PVS verification system. With the abstraction proof rule, proof strategies combining deductive proof construction, model checking, and abstraction can be defined entirely within the PVS framework.
Chapter PDF
References
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proceedings of the 9th Conference on Computer-Aided Verification, CAV’98, LNCS. Springer Verlag, June 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 POPL, January 1977.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.
Michael Colon and Thomas Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Proceedings of the 9th Conference on Computer-Aided Verification, CAV’98, LNCS. Springer Verlag, June 1998.
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving 8CTL*, 9CTL* and CTL*. In ErnstRudiger Olderog, editor, IFIP Conference PROCOMET’94, pages 561–581, 1994.
S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Conference on Computer Aided Verification CAV’97, LNCS 1254, Springer Verlag, 1997.
Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME’ 96, number 1051 in Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.
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, Vol 6, Iss 1, January 1995, 1995.
S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. The PVS Specification Language. Computer Science Laboratory, SRI International, Menlo Park, CA, August 1998.
A. Pardo and G.D. Hachtel. Automatic abstraction techniques for propositional µ-calculus model checking. In Conference on Computer Aided Verification CAV’97, LNCS 1254, Springer Verlag, 1997.
S. Rajan, N. Shankar, and M.K. Srivas. An integration of model checking with automated proof checking. In Computer-Aided Verification, CAV’ 95, number 939 in Lecture Notes in Computer Science, Liège, Belgium, 1995. Springer-Verlag.
John Rushby. Specification, proof checking, and model checking for protocols and distributed systems with PVS. In FORTE/PSTV’ 97, Osaka, Japan, November 1997.
Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß. Case studies in meta-level theorem proving. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs’ 98, volume 1479 of Lecture Notes in Computer Science, pages 461–478, Canberra, Australia, September 1998. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Saïdi, H., Shankar, N. (1999). Abstract and Model Check while You Prove. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_38
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive