opaal: A Prototype Model Checker
- Speaker
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
- Location
Polacksbacken, room 1146
- Abstract
-
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.
- Supervisors
Kim Guldstrand Larsen, René Rydhof Hansen