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- 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 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.

If you would like to cite R2U2, please use our 2023 CAV paper.