Exact Acceleration of Real-Time Model Checking

Martijn Hendriks, Kim G. Larsen

Research output: Contribution to journalArticleAcademicpeer-review

25 Citations (Scopus)
11 Downloads (Pure)

Abstract

Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and that can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effective. We illustrate our exact acceleration technique with run-time data obtained with the model checkers Uppaal and Kronos. Moreover, we demonstrate that automated application of our exact acceleration technique can significantly speed-up the verification of the run-time behavior of LEGO Mindstorms programs.
Original languageEnglish
Pages (from-to)120-139
JournalElectronic notes in theoretical computer science
Volume65
Issue number6
DOIs
Publication statusPublished - 2002
Externally publishedYes

Fingerprint

Dive into the research topics of 'Exact Acceleration of Real-Time Model Checking'. Together they form a unique fingerprint.

Cite this