Options
Runtime Monitoring of c-LTL Specifications on FPGAs Using HLS
Publikationstyp
Conference Paper
Publikationsdatum
2022-06
Sprache
English
Institut
Citation
18th International Conference on Synthesis, Modeling, Analysis and Simulation Methods, and Applications to Circuit Design (SMACD 2022)
Publisher DOI
Scopus ID
2-s2.0-85134761077
Runtime monitoring is a lightweight verification technique that ensures correct execution of a system based on a specification, e. g., in Linear Temporal Logic (LTL). c-LTL is an extended semantics of LTL that speculates on the property's future satisfaction, by this, warning before potentially violating a correctness specification.Our framework generates high-level synthesizable C++ code implementing runtime monitors for c-LTL properties. We evaluate the resource utilization and performance of the monitors obtained from the framework. Synthesis techniques and our dedicated optimizations cut down the required number of LUTs by up to 93%, allowing an effective implementation of runtime monitors.
Schlagworte
counting semantics
LTL
runtime monitoring
runtime verification