Overview

The Realizable, Reconfigurable, Unobtrusive Unit (R2U2) is a stream-based runtime verification framework based on Mission-time Linear Temporal Logic (MLTL) designed to monitor safety-critical or mission-critical systems with constrained computational resources.

Given a specification and input stream, R2U2 will output a stream of verdicts computing whether the specification holds with respect to the input stream. Specifications can be written and compiled using the Configuration Compiler for Property Organization (C2PO).

To get started, go to the Quick Start Guide (C Version) or Quick Start Guide (Rust Version).

If you would like to cite R2U2, please use our 2023 CAV paper [1] and our 2025 NFM Paper [2].

[1]

Chris Johannsen, Phillip Jones, Brian Kempa, Kristin Yvonne Rozier, and Pei Zhang. R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software. In Constantin Enea and Akash Lal, editors, Computer Aided Verification, 483–497. Cham, 2023. Springer Nature Switzerland.

[2]

Alexis Aurandt, Phillip H. Jones, and Kristin Yvonne Rozier. Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust. In Proceedings of the 17th NASA Formal Methods Symposium (NFM 2025), volume TBD of Lecture Notes in Computer Science (LNCS). Williamsburg, Virginia, June 2025. Springer. URL: https://temporallogic.org/research/R2U2Rust/R2U2_Rust_Extended.pdf.