opaal: A Lattice Model Checker

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

DALSGAARD Andreas E. HANSEN Rene R. JOERGENSEN Kenneth Y. LARSEN Kim G. OLESEN Mads Chr. SRBA Jiří

Year of publication 2011
Type Article in Proceedings
Conference Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11)
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.springerlink.com/content/978-3-642-20397-8
Doi http://dx.doi.org/10.1007/978-3-642-20398-5
Field Informatics
Keywords verification; lattice; tool
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.