RAVEN: real-time analyzing and verification environment

DSpace Repository

Show simple item record

dc.contributor Tübingen / Wilhelm-Schickard-Institut für Informatik de_DE
dc.contributor.author Ruf, Jürgen de_DE
dc.date.accessioned 2004-04-26 de_DE
dc.date.accessioned 2014-03-18T10:12:38Z
dc.date.available 2004-04-26 de_DE
dc.date.available 2014-03-18T10:12:38Z
dc.date.issued 2000 de_DE
dc.identifier.other 111265908 de_DE
dc.identifier.uri http://nbn-resolving.de/urn:nbn:de:bsz:21-opus-12061 de_DE
dc.identifier.uri http://hdl.handle.net/10900/48593
dc.description.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. en
dc.language.iso en de_DE
dc.publisher Universität Tübingen de_DE
dc.rights ubt-nopod de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_ubt-nopod.php?la=de de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_ubt-nopod.php?la=en en
dc.subject.classification Tübingen / Wilhelm-Schickard-Institut für Informatik de_DE
dc.subject.ddc 004 de_DE
dc.title RAVEN: real-time analyzing and verification environment en
dc.type Report (Bericht) de_DE
dc.date.updated 2012-10-11 de_DE
utue.publikation.fachbereich Sonstige - Informations- und Kognitionswissenschaften de_DE
utue.publikation.fakultaet 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE
dcterms.DCMIType Text de_DE
utue.publikation.typ report de_DE
utue.opus.id 1206 de_DE
utue.opus.portal wsi de_DE
utue.opus.portalzaehlung 2000.03000 de_DE
utue.publikation.source WSI ; 2000 ; 3 de_DE
utue.publikation.reihenname WSI-Reports - Schriftenreihe des Wilhelm-Schickard-Instituts für Informatik de_DE
utue.publikation.zsausgabe 2000, 3
utue.publikation.erstkatid 2919855-0


This item appears in the following Collection(s)

Show simple item record