Abstract
This paper gives a short overview of 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. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Beyer, D., Lewerentz, C., & Noack, A. (2003). Rabbit: A tool for BDD-based verification of real-time systems. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 122–125. https://doi.org/10.1007/978-3-540-45069-6_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
