Rabbit and Cottbus Timed Automata

Software Systems Engineering Research Group
Brandenburg Technical University Cottbus, Germany

Objectives

Modular specification of real-time systems based on timed (and hybrid) automata: CottbusTimed Automata.
Efficient reachability analysis and refinement check for Cottbus Timed Automata: Rabbit.

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:

Microsoft Windows (9x, NT, 2000)
Sun Solaris 2.6 (SunOS 5.6)
GNU/Linux

Download the tool Rabbit and example models.
Video: Case Study Production Cell (YouTube).

Publications

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

Beyer, Dirk; Noack, Andreas. Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification? FORTE 2003.
Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols.
Beyer, Dirk; Lewerentz, Claus; Noack, Andreas. Rabbit: A Tool for BDD-based Verification of Real-Time Systems. CAV 2003.
A description of the BDD-based tool's main features.
Beyer, Dirk. Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata. Mensch & Buch Verlag, Berlin, Dissertation, 2002.
Dissertation, describes all important concepts and details of the Rabbit project in german.
Beyer; Dirk. Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs. CHARME 2001.
Decribes how the tool checks refinement via simulation relation.
Beyer, Dirk; Rust, Heinrich: Cottbus Timed Automata: Formal Definition and Semantics. FSCBS 2001.
The full formal definition and semantics of CTA.
Beyer, Dirk: Improvements in BDD-based Reachability Analysis of Timed Automata. FME 2001.
About the BDD-based representation: proof of an upper bound for the BDD of the transition relation, variable ordering, heuristics for efficient verification, contains the proof of the equivalence of our integer semantics to the continuous semantics regarding reachable locations.
Beyer, Dirk; Rust, Heinrich: A Tool for Modular Modelling and Verification of Hybrid Systems. WRTP 2000.
The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.
Beyer, Dirk; Lewerentz, Claus; Rust, Heinrich: Modelling and Analysing a Railroad Crossing in a Modular Way. FMICS 2000.
Describes a case study for modeling and analysis using the DDM-based representation.
Beyer, Dirk; Rust, Heinrich: Modeling a Production Cell as a Distributed Real-Time System with Cottbus Timed Automata. FBT 1998.
The first published paper where we introduce the concepts of Cottbus Timed Automata, i.e. modules, interfaces and a modeling example.

Project Team

Dirk Beyer (postdoctoral researcher)
Andreas Noack (research assistant)
Andy Heinig (student)
Michael Vogel (student)

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