Abstract
We address the problem of verifying systems operating on different types of variables ranging over infinite domains. We consider in particular systems modeled by means of extended automata communicating through unbounded fifo channels. We develop a general methodology for analyzing such systems based on combining automatic generation of abstract models (not necessarily finite-state) with symbolic reachability analysis. Reachability analysis procedures allow to verify automatically properties at the abstract level as well as to generate auxiliary invariants and accurate abstraction functions that can be used at the concrete level. We propose a realization of this approach in a framework which extends PVS with automatic invariant checking strategies, automatic procedures for generating abstract models, as well as automatabased decision procedures and reachability analysis procedures for fifo channels systems.
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
P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In TACAS’99. LNCS 1579, 1999. 149, 154
P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In CAV’98. LNCS 1427, 1998. 147, 149, 154, 154, 154
P.A. Abdulla and B. Jonsson. Verifying Programs with Unreliable Channels. Inform. and Comput., 127(2):91–101, 1996. 147
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The Algorithmic Analysis of Hybrid Systems. TCS, 138, 1995. 147
S. Bensalem, Y. Lakhnech, and S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In CAV’98. LNCS 1427, 1998. 147, 148, 151
S. Bensalem, Y. Lakhnech, and S. Owre. InVeSt: A Tool for the Verification of Invariants. In CAV’98. LNCS 1427, 1998. 147, 148
B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. In CAV’96. LNCS 1102, 1996. 147, 154
B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets. In CAV’94. LNCS 818, 1994. 147, 154
A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR’97. LNCS 1243, 1997. 147
A. Bouajjani and P. Habermehl. Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. In ICALP’97. LNCS 1256, 1997. 147
Gérard Cécé, Alain Finkel, and S. Purushothaman Iyer. Unreliable Channels Are Easier to Verify Than Perfect Channels. Inform. and Comput., 124(1):20–31, 1996. 154
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM TOPLAS, 16(5), 1994. 147, 151
P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. In IFIP Conf. on Formal Description of Programming Concepts. North-Holland Pub., 1977. 147, 150, 154
P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In POPL’78. ACM, 1978. 147
D. Dams, R. Gerth, and O. Grumberg. Generation of ReducedModels for Checking Fragments of CTL. In CAV’93. LNCS 697, 1993. 147
P. D’Argenio, J-P. Katoen, T. Ruys, and G.J. Tretmans. The Bounded Retransmission Protocol must be on Time. In TACAS’97. LNCS 1217, 1997. 156
A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems. In Infinity’97, 1997. 147
S. Graf and C. Loiseaux. A Tool for Symbolic Program Verification and Abstraction. In CAV’93. LNCS 697, 1993. 147
S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In CAV’97, volume 1254 of LNCS, 1997. 147
J-F. Groote and J. van de Pol. A Bounded Retransmission Protocol for Large Data Packets. In AMAST’96. LNCS 1101, 1996. 156
L. Helmink, M.P.A. Sellink, and F. Vaandrager. Proof checking a Data Link Protocol. In Types for Proofs and Programs. LNCS 806, 1994. 156
R.M. Karp and R.E. Miller. Parallel Program Schemata: A Mathematical Model for Parallel Computation. In Switch. and Automata Theory Symp. IEEE, 1967. 154
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property Preserving Abstractions for the Verification of Concurrent Systems. FMSD, 6(1), 1995. 147, 150, 151
Oliver Matz, Axel Miller, Andreas Potthoff, Wolfgang Thomas, and Erich Valkema. Report on the Program AMoRE. Technical Report 9507, Inst. f. Informatik u. Prakt. Math., CAU Kiel, 1995. 149, 153
O. Müller and T. Nipkow. Combining Model Checking and Deduction for I/OAutomata. In TACAS’95. LNCS 1019, 1995. 152
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, Feb. 1995. 148
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
Abdulla, P.A., Annichini, A., Bensalem, S., Bouajjani, A., Habermehl, P., Lakhnech, Y. (1999). Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. 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_15
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_15
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