opaal: A Prototype Model Checker
Mads Christian Olesen
PhD student in the Distributed and Embedded Systems group at the Department of Computer Science, Aalborg University
- Date and Time
Thursday, June 16th, 2011 at 13:30
Polacksbacken, room 1146
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. Lattice automata generalise, among others, timed automata.
The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features, and is designed to allow for rapid prototyping while being easy to learn and sufficiently fast. For these reasons it is implemented in Python.
Currently, opaal is still a work in progress; it has nevertheless been used successfully by students to try out a new data structure for clocks.
Kim Guldstrand Larsen, René Rydhof Hansen