This project implements a runtime monitoring component for the Caravel SoC that is capable of monitoring a temporal logic safety property. The component has two SRAM blocks for storing its configuration (1 kB and 2 kB each) and implements a lookup table-based approach to monitoring a reactive system.
Many modern reactive systems, such as those implemented using microcontrollers or system on chips (SoCs) need to be behave correctly in all situations in order for them to be usable. It not always possible to verify the implementation of a reactive system upfront before its deployment. The research area of runtime verification deals with approaches to detect specification violations at runtime, so that they can at least be detected after deployment of the reactive system. With a reported specification violation, the system's implementation can then be revised or the system can switch to a fail-safe mode.
Runtime verification techniques typically need to be lightweight, i.e., they should not slow down the monitored system too much. Especially for monitoring temporal specifications that describe how the system evolves and reacts over time, implementing efficient monitors is far from trivial. Such specification can for example be given in linear temporal logic (LTL). Previous approaches to monitoring such specifications have mostly relied on either:
Solution 1 is mostly suitable for bigger embedded systems that actually employ real-time operating systems, and it requires a careful selection of what exactly is monitored in order for the monitoring process not to require too much computation time. Solution 2 is quite expensive, as the FPGA chip can be more costly than the microcontroller/SoC being monitored. In solution 3, the overhead due to the added instructions can be quite substantial.
A specialized runtime monitoring component for microcontrollers, as implemented in this project, can help to reduce monitoring overhead. Once programmed, the component performs the monitoring process on its own, while the microcontroller/SoC only needs to send the elements of the system execution to be monitored to the component by writing to one of its control registers via the bus connecting the SoC core and the monitoring component.
This is a specialized on-chip microcontroller/SoC component for performing runtime monitoring of temporal logic formulas. The component executes a monitor that has been compiled using a specialized compiler and uploaded to the component's SRAMs. After initialization, there is a specific address in the address space of the SoC to which the current valuation of the propositions to be monitored can be written - updating the runtime monitor is then done by the monitor component.