Rabbit

Rabbit: A tool for BDD-based verification of real-time systems. 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


References in zbMATH (referenced in 23 articles , 1 standard article )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Norman, Gethin; Parker, David; Sproston, Jeremy: Model checking for probabilistic timed automata (2013)
  2. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  3. Nguyen, Truong Khanh; Sun, Jun; Liu, Yang; Dong, Jin Song; Liu, Yan: Improved BDD-based discrete analysis of timed systems (2012)
  4. Fisher, Michael: An introduction to practical formal methods using temporal logic (2011)
  5. Sherif, Adnan; Cavalcanti, Ana; Jifeng, He; Sampaio, Augusto: A process algebraic framework for specification and validation of real-time systems (2010)
  6. Hasan, Osman; Tahar, Sofiène: Performance analysis and functional verification of the stop-and-wait protocol in HOL (2009)
  7. Thomas, Dina; Chakraborty, Supratik; Pandya, Paritosh: Efficient guided symbolic reachability using reachability expressions (2008)
  8. Kwiatkowska, Marta; Norman, Gethin; Parker, David; Sproston, Jeremy: Performance analysis of probabilistic timed automata using digital clocks (2006)
  9. Thomas, Dina; Chakraborty, Supratik; Pandya, Paritosh: Efficient guided symbolic reachability using reachability expressions (2006)
  10. Duflot, Marie; Fribourg, Laurent; Hérault, Thomas; Lassaigne, Richard; Magniette, Frédéric; Messika, Stéphane; Peyronnet, Sylvain; Picaronny, Claudine: Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. (2005)
  11. Rust, Heinrich: Operational semantics for timed systems. A non-standard approach to uniform modeling of timed and hybrid systems. (2005)
  12. Yan, Rongjie; Li, Guangyuan; Tang, Zhisong: Symbolic model checking of finite precision timed automata (2005)
  13. Dutertre, Bruno; Sorea, Maria: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata (2004)
  14. Panangaden, Prakash (ed.); van Breugel, Franck (ed.): Mathematical techniques for analyzing concurrent and probabilistic systems. (2004)
  15. Półrola, Agata; Penczek, Wojciech; Szreter, Maciej: Towards efficient partition refinement for checking reachability in timed automata (2004)
  16. Beyer, Dirk; Lewerentz, Claus; Noack, Andreas: Rabbit: A tool for BDD-based verification of real-time systems. (2003)
  17. Beyer, Dirk; Noack, Andreas: Can decision diagrams overcome state space explosion in real-time verification? (2003)
  18. Seshia, Sanjit A.; Bryant, Randal E.: Unbounded, fully symbolic model checking of timed automata using Boolean methods. (2003)
  19. Kwiatkowska, Marta; Norman, Gethin; Pacheco, António: Model checking CSL until formulae with random time bounds (2002)
  20. Kwiatkowska, Marta; Norman, Gethin; Sproston, Jeremy: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol (2002)

1 2 next


Further publications can be found at: http://www.sosy-lab.org/~dbeyer/Publications/bib/Author/BEYER-D.html