From Natural Language Requirements to Runtime Monitors for Resource-Constrained Systems: Integrating FRET and R2U2

The Realizable, Responsive, Unobtrusive Unit (R2U2) is a stream-based runtime monitoring framework that verifies a system’s adherence to a set of formal system requirements with minimal resource overhead, allowing for real-time, online monitoring on resource-constrained systems. Yet, a persisting challenge for deploying runtime monitors is eliciting formal specifications that accurately capture system requirements commonly expressed in ambiguous natural language; therefore, we employ NASA’s Formal Requirements Elicitation Tool (FRET) to configure R2U2 monitors from structured natural language requirements. We extend FRET to formalize requirements in Mission-time Linear Temporal Logic (MLTL) - the native specification logic of R2U2, and we provide 157 MLTL rewrite rules that reduce each of FRET’s MLTL formalizations by an average of 15 operators, or 36.05%, decreasing the resources necessary to monitor these requirements with R2U2. We also introduce a novel SMT-based proof technique for automatically proving the correctness of these rewrite rules.