RAVEN: Real-time analyzing and verification environment. 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 for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Cansell, Dominique; Méry, Dominique; Proch, Cyril: System-on-chip design by proof-based refinement (2009)
- Markey, Nicolas; Schnoebelen, Philippe: Symbolic model checking for simply-timed systems (2004)
- Flake, Stephan; Mueller, Wolfgang: Formal semantics of static and temporal state-oriented OCL constraints (2003)
- Ruf, Jürgen; Kropf, Thomas: Symbolic verification and analysis of discrete timed systems (2003)
- Flake, Stephan; Mueller, Wolfgang: A UML profile for real-time constraints with the OCL (2002)
- Reif, Wolfgang; Schellhorn, Gerhard; Vollmer, Tobias; Ruf, Jürgen: Correctness of efficient real-time model checking (2001)
- Ruf, Jürgen: RAVEN: Real-time analyzing and verification environment (2001)
- Ruf, Jürgen; Kropf, Thomas: Formal verification of discrete real-time systems (2001)