Runtime verification involves checking whether a given system (in software or hardware) satisfies a given property during the execution of the system. This paper presents a set of runtime verification algorithms, their correctness, and complexity, as well as their realization in field-programmable gate array (FPGA) hardware. The properties verified are temporal properties expressed in past time metric temporal logic, and the system is an embedded system required to satisfy timing properties. The discrete model of time is used in the paper.

The paper is quite comprehensive and balanced since it is rich in theoretical results like correctness and complexity bounds as well as practical realization of the algorithms. It is very useful for researchers working in the area of runtime verification systems and formal methods. Due to the many illustrative examples, I believe that practitioners interested in rigorous development of embedded systems would also find the paper useful. The paper could have been split into two, one dealing with theoretical aspects and the other focusing on practical aspects. By covering these aspects together, I hope that the paper has not lost both types of readers.