Rabbit and Cottbus Timed Automata

Software Systems Engineering Research Group
Brandenburg Technical University Cottbus, Germany


Rabbit is a model checking tool for real-time systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data structure BDD. Good variable orderings for the BDDs are computed from the modular structure of the model and an estimate of the BDD size. This leads to a significant performance improvement compared to the tool RED and the BDD-based version of Kronos.

Rabbit - Release 2.1

The tool is free software, released under the Apache 2.0 license.
Rabbit is available for the following platforms: Download the tool Rabbit and example models.
Video: Case Study Production Cell (YouTube).


Full references of the papers and electronic versions for download you can find on our Publications page.

Project Team

Author: Dirk Beyer, my project pages: BLAST, CCVisu, Chic, CrocoPat, CSIsat, Rabbit