Tags:Generic re-programmable monitors, Hardware monitors and LTL monitor construction
Abstract:
Runtime Verification (RV) is a semi-formal verification technique that involves augmenting a system with runtime monitors that continuously check for deviations from the system’s expected behavior. This ensures that the current run of the system is error-free. State-of-the-art RV frameworks synthesize runtime monitors from formal specifications of system properties. As a result, these monitors are tailored for single-property verification, necessitating resynthesis for different properties. In this work, we propose a RV framework that includes a domain-specific architecture and its associated compiler that takes as input properties specified in Linear Temporal Logic (LTL) and flags deviations from the expected behavior of a system. Our proposed framework requires only recompilation (instead of resynthesis) as properties change, thereby enabling an ASIC implementation of the runtime monitors. This allows for high-speed, low-overhead as well as flexible monitoring of a wide range of system properties. This level of flexibility is essential for ensuring the reliability and robustness of complex systems. We evaluate our framework using 53 LTL properties from several prior works.
FaRM-LTL: a Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL Properties