Form Methods Syst Des (2014) 44:203–239 DOI 10.1007/s10703-013-0199-z Runtime verification of embedded real-time systems

© The Author(s) 2013. This article is published with open access at Springerlink.com 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 de-sign 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 effi-cient 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 consid-ered, the time-bounded Since operator, we obtain a time complexity that is doubly logarith-mic 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