title: Runtime verification of embedded real-time systems.
abstract: We present a runtime verification framework that allows on-line monitoring of past-time Metric Temporal Logic (ptMTL) specifications in a discrete time setting. We design observer algorithms for the time-bounded modalities of ptMTL, which take advantage of the highly parallel nature of hardware designs. The algorithms can be translated into efficient hardware blocks, which are designed for reconfigurability, thus, facilitate applications of the framework in both a prototyping and a post-deployment phase of embedded real-time systems. We provide formal correctness proofs for all presented observer algorithms and analyze their time and space complexity. For example, for the most general operator considered, the time-bounded Since operator, we obtain a time complexity that is doubly logarithmic both in the point in time the operator is executed and the operator's time bounds. This result is promising with respect to a self-contained, non-interfering monitoring approach that evaluates real-time specifications in parallel to the system-under-test. We implement our framework on a Field Programmable Gate Array platform and use extensive simulation and logic synthesis runs to assess the benefits of the approach in terms of resource usage and operating frequency.
authors.affiliation: Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Thomas
authors.initials: T
authors.lastname: Reinbacher
authors.affiliation: Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
authors.forename: Matthias
authors.initials: M
authors.lastname: Függer
authors.affiliation: Embedded Software Laboratory, RWTH Aachen University and Verified Systems International GmbH, Am Fallturm 1, 28359 Bremen, Germany.
authors.forename: Jörg
authors.initials: J
authors.lastname: Brauer
keywords: Embedded real-time systems; Online monitoring; Past-time logics; Runtime verification