Modular specification of real-time systems based
timed (and hybrid) automata: CottbusTimed Automata.
Efficient reachability analysis and refinement
for Cottbus Timed Automata: Rabbit.
Rabbit is a model checking tool for
systems. The modeling language are timed automata extended with
for modular modeling. The tool provides reachability analysis and
checking, both implemented using the data structure BDD. Good variable
orderings for the BDDs are computed from the modular structure of the
and an estimate of the BDD size. This leads to a significant
improvement compared to the tool RED and the BDD-based version of
Rabbit - Release 2.1
The tool is free software, released under the Apache 2.0 license.
Rabbit is available for the following platforms:
Full references of the papers and electronic
for download you can find on our Publications
Beyer, Dirk; Noack, Andreas. Can Decision
Overcome State Space Explosion in Real-Time Verification? FORTE
Analysis of the efficiency of binary
decision diagrams (BDDs) and clock
difference diagrams (CDDs) in the verification of timed automata.
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
A description of the BDD-based tool's
Beyer, Dirk. Formale Verifikation von
mittels Cottbus Timed Automata. Mensch & Buch Verlag,
Dissertation, describes all important
details of the Rabbit project in german.
Beyer; Dirk. Efficient Reachability
Refinement Checking of Timed Automata using BDDs. CHARME 2001.
Decribes how the tool checks
refinement via simulation
Beyer, Dirk; Rust, Heinrich: Cottbus Timed
Formal Definition and Semantics. FSCBS 2001.
The full formal definition and
semantics of CTA.
Beyer, Dirk: Improvements in BDD-based
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
of our integer semantics to the continuous semantics regarding
Beyer, Dirk; Rust, Heinrich: A Tool for
and Verification of Hybrid Systems. WRTP 2000.
The reference for the first version of
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
using the DDM-based representation.
Beyer, Dirk; Rust, Heinrich: Modeling a
Cell as a Distributed Real-Time System with Cottbus Timed Automata.
The first published paper where we
concepts of Cottbus Timed Automata, i.e. modules, interfaces and a