r2u2_cli
The Realizable Responsive Unobtrusive Unit is an online runtime monitor framework.
Science Score: 67.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 1 DOI reference(s) in README -
✓Academic publication links
Links to: springer.com -
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (12.0%) to scientific vocabulary
Repository
The Realizable Responsive Unobtrusive Unit is an online runtime monitor framework.
Basic Info
- Host: GitHub
- Owner: R2U2
- License: apache-2.0
- Language: Python
- Default Branch: develop
- Homepage: https://r2u2.temporallogic.org
- Size: 40.5 MB
Statistics
- Stars: 10
- Watchers: 3
- Forks: 1
- Open Issues: 18
- Releases: 1
Metadata Files
README.md
About
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).
If you would like to cite R2U2, please use our 2023 CAV paper (.bib) and 2025 NFM paper (.bib).
Requirements
The following dependencies are required to run C2PO:
- Python 3.9 or greater
- (Optional) To enable satisfiability checking, install Z3 or any other SMTLIB2-compatible solver.
- (Optional) To enable equality saturation, first install Rust then install egglog via the compiler/setup_egglog.sh script.
The following dependencies are required to run R2U2 C version: - Make - C99 compiler
The following dependencies are required to run R2U2 Rust version: - Rust 1.82.0 or greater
Building
R2U2 C Version
To build R2U2, run make from monitors/c/:
bash
cd monitors/c/
make
This only needs to be once, regardless of the specifications you wish to monitor.
R2U2 Rust Version
To build R2U2 from source, run cargo build --release from monitors/r2u2_cli:
bash
cd monitors/rust/r2u2_cli/
cargo build --release
This only needs to be once, regardless of the specifications you wish to monitor.
***There is also a r2u2_cli Rust crate available to run C2PO and R2U2.
Running
Running R2U2 requires a specification and an input stream. To monitor the specification
defined in examples/simple.c2po using
examples/simple.csv as an input stream:
Compile the specification using C2PO
bash python3 compiler/c2po.py --output spec.bin --map examples/simple.map examples/simple.c2poRun R2U2 using the compiled specification and the input stream
a. Run R2U2 C version:
bash ./monitors/c/build/r2u2 spec.bin < examples/simple.csvb. Run R2U2 Rust version:bash ./monitors/rust/r2u2_cli/target/release/r2u2_cli run spec.bin examples/simple.csv
Output
The output of R2U2 is a verdict stream with one verdict per line. A verdict includes a formula ID, timestamp, and truth value. Formula IDs are determined by the order in which they are defined in the specification file. Verdicts are aggregated so that if R2U2 can determine a range of values with the same truth at once, only the last time is output.
The following is a stream where formula 0 is true from 0-7 and false from 8-11 and formula 1 is false from times 0-4:
0:7,T
1:4,F
0:11,F
Examples
Example specifications and traces can be found in the examples/, test/,
and compiler/test/ directories.
The benchmarks/ directory includes sets of larger specifications taken from various
sources. See each sub-directory's README for its description and source.
Documentation
The documentation for R2U2 can be found here. The documentation includes user and developer guides for both R2U2 and C2PO.
Support
If you have a question about running R2U2, please open a "Question" issue.
If you believe you have found a case of unsound output from R2U2, please refer to CONTRIBUTING.md and open a "Bug Report" issue.
License
Licensed under either of
- Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.
Owner
- Name: R2U2
- Login: R2U2
- Kind: organization
- Repositories: 8
- Profile: https://github.com/R2U2
Citation (CITATION.bib)
@InProceedings{r2u2,
author="Johannsen, Chris
and Jones, Phillip
and Kempa, Brian
and Rozier, Kristin Yvonne
and Zhang, Pei",
editor="Enea, Constantin
and Lal, Akash",
title="R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software",
booktitle="Computer Aided Verification",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="483--497",
abstract="R2U2 is a modular runtime verification framework capable of monitoring sets of specifications in real time and in resource-constrained environments. Such environments demand that a runtime monitor be fast, easily integratable, accessible to domain experts, and have predictable resource requirements. Version 3.0 adds new features to R2U2 and its associated suite of tools that meet these needs including a new front-end compiler that accepts a custom specification language, a GUI for resource estimation, and improvements to R2U2's internal architecture.",
isbn="978-3-031-37709-9"
}
GitHub Events
Total
- Create event: 18
- Release event: 1
- Issues event: 21
- Watch event: 9
- Delete event: 5
- Issue comment event: 26
- Public event: 1
- Push event: 193
- Pull request review comment event: 97
- Pull request review event: 94
- Pull request event: 24
- Fork event: 1
Last Year
- Create event: 18
- Release event: 1
- Issues event: 21
- Watch event: 9
- Delete event: 5
- Issue comment event: 26
- Public event: 1
- Push event: 193
- Pull request review comment event: 97
- Pull request review event: 94
- Pull request event: 24
- Fork event: 1
Issues and Pull Requests
Last synced: 10 months ago
All Time
- Total issues: 13
- Total pull requests: 13
- Average time to close issues: 2 months
- Average time to close pull requests: 6 days
- Total issue authors: 2
- Total pull request authors: 3
- Average comments per issue: 0.38
- Average comments per pull request: 0.69
- Merged pull requests: 7
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 13
- Pull requests: 13
- Average time to close issues: 2 months
- Average time to close pull requests: 6 days
- Issue authors: 2
- Pull request authors: 3
- Average comments per issue: 0.38
- Average comments per pull request: 0.69
- Merged pull requests: 7
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- cgjohannsen (9)
- aaurandt (4)
Pull Request Authors
- cgjohannsen (7)
- aaurandt (5)
- AeRosentrater (1)
Top Labels
Issue Labels
Pull Request Labels
Packages
- Total packages: 2
-
Total downloads:
- cargo 8,657 total
-
Total dependent packages: 0
(may contain duplicates) -
Total dependent repositories: 0
(may contain duplicates) - Total versions: 17
- Total maintainers: 1
crates.io: r2u2_cli
R2U2 CLI: A stream-based runtime monitor command-line interface
- Homepage: https://r2u2.temporallogic.org
- Documentation: https://docs.rs/r2u2_cli/
- License: MIT OR Apache-2.0
-
Latest release: 4.0.0
published 12 months ago
Rankings
Maintainers (1)
crates.io: r2u2_core
R2U2: A stream-based runtime monitor in no_std
- Homepage: https://r2u2.temporallogic.org
- Documentation: https://docs.rs/r2u2_core/
- License: MIT OR Apache-2.0
-
Latest release: 4.0.0
published 12 months ago
Rankings
Maintainers (1)
Dependencies
- actions/checkout v4 composite
- actions/configure-pages v3 composite
- actions/deploy-pages v4 composite
- actions/setup-python v3 composite
- actions/upload-pages-artifact v3 composite
- actions/checkout v3 composite
- actions/setup-python v3 composite
- Sphinx *
- breathe *
- exhale *
- myst-parser *
- sphinx-book-theme *
- sphinx-collections *
- sphinxcontrib-bibtex *
- tqdm * test