Runtime Monitoring of c-LTL Specifications on FPGAs Using HLS

Publikationstyp
Conference Paper
Publikationsdatum
2022-06
Sprache
English
Author
Martino, Gianluca orcid-logo
Fey, Görschwin orcid-logo
Institut
Eingebettete Systeme E-13 
TORE-URI
http://hdl.handle.net/11420/13322
Citation
18th International Conference on Synthesis, Modeling, Analysis and Simulation Methods, and Applications to Circuit Design (SMACD 2022)
Contribution to Conference
18th International Conference on Synthesis, Modeling, Analysis and Simulation Methods, and Applications to Circuit Design, SMACD 2022 
Publisher DOI
10.1109/SMACD55068.2022.9816308
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