RAVEN: real-time analyzing and verification environment

Abstract

Formal verification has become an important task in the design of systems. Techniques like symbolic model checking have reached industrial applicability. These techniques are well suited for fully synchronous systems modeled with qualitative time (clock cycles). If systems are embedded in a real-time environment and upper bounds for reaction times are important to guarantee a proper and save functionality, the verification of real-time properties is very important. We target at this application area with our tool RAVEN. RAVEN is a real-time model checker extended by analysis algorithms. The system description is specified as a network of communicating parallel working real-time processes. Each process is a time extended finite state machine (I/O-interval structure [1,2]). The properties are specified in the quantitative temporal logic CCTL. RAVEN provides different algorithms to determine critical delay times of the design. The queries for the analysis capabilities cover minimum, maximum and maximal stability computations. RAVEN is able to generate counter examples and witnesses for CCTL formulas. Analysis results can be visualized by traces. All traces are graphically presented in an integrated wave form browser. Moreover, RAVEN offers additional checks. For instance, it can detect dead- and live locks and visualizes traces to these "locks" in its integrated wave form browser tool. It is also possible to generate random simulations of the composed system. RAVEN uses MTBDDs [5,6] for a symbolic representation of the systems [8]. This data structure results in a compact system representation and efficient verification algorithms. All algorithms are alternatively implemented for an ROBDD [7] representation.