Abstract
In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.
Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ 1, ..., g4 l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕ i or ¬ϕ i is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.
Chapter PDF
References
N. Bjorner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H. Sipma, and T. Uribe. Step: Deductive-algorithmic verification of reactive and realtime systems. In CAV'96. LNCS 1102, 1996.
K. Baukus, S. Bensalem, and Y. Lakhnech. A PVS based tool for the verification of invariants. submitted to CAV'97.
S. Bensalem, Y. Lakhnech, and H. Saidi, Powerful techniques for the automatic generation of invariants. In CAV'96, LNCS 1102, 1996.
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), 1994.
K. M. Chandy and J. Misra. Parallel Program Design. 1988.
D. Dams. Abstract interpretation and partition refinement for model checking. Phd Thesis, Technical University of Eindhoven, July 1996.
J. Dingel and Th. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In CAV'95. LNCS 939, 1995.
D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In CAV'93, LNCS 697, 1993.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, LNCS 1066, 1996.
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier and M. Sighireanu. CADP (Caesar/Aldébaran Development Package): A protocol validation and verification toolbox. In CAV'96. LNCS 1102.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV'93. LNCS 697, 1993.
S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. accepted to Distributed Computing.
S. Graf and H. Saidi. Verifying invariants using theorem proving. In CAV'96, LNCS 1102, 1996.
J.F Groote and J. van de Pol. A bounded retransmission protocol for large data packets. Technical Report Logic Group 100, Utrecht University, 1993.
H. Hungar, O. Grumberg, and W. Damm. What if model checking must be truly symbolic. In TACAS'95. LNCS 1019, 1995.
T. Henzinger and P.H. Ho. Hytech: the Cornell hybrid technology tool. In Hybrid Systems II. LNCS 999, 1995.
N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In SAS'94. LNCS 864.
K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods in Europe'96, 1996.
L. Helmink, M. Sellink, and F. Vaandrager. Proof-checking a data link protocol. Technical report CS-R9420, CWI, 1994.
P. Kelb, D. Dams, and R. Gerth. Efficient symbolic model-checking for the full μ-calculus using compositional abstractions. Tech Rep 31, TU Eindhoven, 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, Vol 6, Iss 1, 1995
H. Saïdi. The invariant checker: Automated deductive verification of reactive systems. In this volume.
Joseph Sifakis. A unified approach for studying the properties of transition systems. TCS 18, 1982.
N. Shankar, S. Owre, and J.M. Rushby. A Tutorial on Specification and Verification using PVS. SRI International, Menlo Park, CA, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, S., Saidi, H. (1997). Construction of abstract state graphs with PVS. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive