RAVEN: Real-Time Analyzing and Verification Environment
| dc.creator | Ruf,Jürgen | |
| dc.date | 2001 | |
| dc.date.accessioned | 2024-02-06T12:51:04Z | |
| dc.date.available | 2024-02-06T12:51:04Z | |
| dc.description | 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. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-007-01-0089 | |
| dc.identifier | https://lib.jucs.org/article/27766/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7908 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 7(1): 89-104 | |
| dc.subject | formal verification | |
| dc.subject | model checking | |
| dc.subject | analysis | |
| dc.subject | real-time systems | |
| dc.title | RAVEN: Real-Time Analyzing and Verification Environment | |
| dc.type | Research Article |