Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 7 / Issue 1

available in:   PDF (147 kB) PS (109 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-007-01-0089


RAVEN: Real-Time Analyzing and Verification Environment

J├╝rgen Ruf (University of Tuebingen, Germany)

Abstract: In this paper we present the real-time verification and analysis tool RAVEN. RAVEN is developed for verifying timed systems on various levels of abstraction. It integrates a real-time model checker for real-time specifications, it offers algorithms for analyzing critical delay times, for inspecting data values and event occurrences and for detecting dead_locks and live-locks. The counter example generator provides helpful information for error recovering by printing system execution paths (failing a given specification) to the integrated wave_form browser. All included algorithms are based on a common data structure enabling a compact representation and possibilities for acceleration. By some examples we show that our approach outperforms some state-of-the-art verification tools.

Keywords: analysis, formal verification, model checking, real-time systems

Categories: C.3, F.3.1, I.6.4