Improving Flexibility in Embedded System Runtime Verification with Python

A dynamic reconfigurable embedded system runtime verification framework Hat-RV based on hardware-assisted tracing is proposed for resource-constrained embedded systems. Hardware-assisted tracing reduces the overhead of obtaining detailed program execution information. Hat-RV reconstructs the program trajectory through real-time online analysis of trace data to further support runtime verification. At the same time, taking advantage of the PYNQ architecture, the overall framework of Hat-RV is abstracted into an Overlay, where the monitor modules can be dynamically loaded to change the properties of the verification at runtime. The user can achieve the monitoring loading and Overlay mapping simply through the Python interface, thereby increasing the flexibility of runtime verification of embedded systems.