We present an algorithmic framework that allows on-line monitoring of past-time MTL specifications in a discrete time setting. The algorithms allow to be synthesized into efficient observer hardware blocks, which take advantage of the highly-parallel nature of hardware designs. For the time-bounded Since operator of past-time MTL we obtain a time complexity that is double logarithmic in the time it is executed at and the given time bounds of the Since operator.
This result is promising with respect to a non-interfering monitoring approach that evaluates real-time specifications during the execution of the system-under-test. The resulting hardware blocks are reconfigurable and have applications in prototyping and runtime verification of embedded real-time systems.
Thomas Reinbacher, Matthias Függer, Jörg Brauer: Real-Time Runtime Verification on Chip. In 3rd International Conference on Runtime Verification (RV), Istanbul, Turkey, 2012.