opaal: A Lattice Model Checker. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Al-Bataineh, Omar; Reynolds, Mark; French, Tim: Finding minimum and maximum termination time of timed automata models with cyclic behaviour (2017)
- Adzkiya, Dieky; De Schutter, Bart; Abate, Alessandro: Computational techniques for reachability analysis of Max-Plus-Linear systems (2015)
- Al-Bataineh, Omar; Reynolds, Mark; French, Tim: Accelerating worst case execution time analysis of timed automata models with cyclic behaviour (2015)
- Al-Bataineh, Omar; Reynolds, Mark; French, Tim: Finding best and worst case execution times of systems using difference-bound matrices (2014)
- Dalsgaard, Andreas E.; Laarman, Alfons; Larsen, Kim G.; Olesen, Mads Chr.; van de Pol, Jaco: Multi-core reachability for timed automata (2012)
- Dalsgaard, Andreas Engelbredt; Hansen, René Rydhof; Jørgensen, Kenneth Yrke; Larsen, Kim Gulstrand; Olesen, Mads Chr.; Olsen, Petur; Srba, Jiří: opaal: A lattice model checker (2011) ioport