Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
opaal: A Lattice Model Checker
verfasst von : Andreas Engelbredt Dalsgaard, René Rydhof Hansen, Kenneth Yrke Jørgensen, Kim Gulstrand Larsen, Mads Chr. Olesen, Petur Olsen, Jiří Srba
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
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 present a new open source model checker,
opaal
, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction by using a method similar to Counter-Example Guided Abstraction Refinement. The
opaal
engine supports a subset of the UPPAAL timed automata language extended with lattice features. We report on the status of the first public release of
opaal
, and demonstrate how
opaal
can be used for efficient verification on examples from domains such as database programs, lossy communication protocols and cache analysis.