1999 | OriginalPaper | Buchkapitel
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis
verfasst von : Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.