RiTHM

The tool RiTHM (Runtime Time-triggered Heterogeneous Monitoring) is a prototype implementation of the group's work on runtime monitoring including work on time-triggered monitoring, power-aware monitoring, and accelerator technology for monitoring.

The tool RiTHM takes a C program under inspection and a set of LTL properties as input and generates an instrumented C program that is verified at run time by a time-triggered monitor. The output C program can be instrumented in two ways: (1) it is monitored in a time-triggered fashion with a fixed polling period, or (2) the monitor is augmented with PID or fuzzy controllers that ensure minimum variation in monitor polling period while maximizing memory utilization. In both cases, the monitor is invoked in a time-triggered fashion, ensuring that the states of the program can be reconstructed at each invocation by using efficient instrumentation. The monitor verification decision procedure is sound and complete and takes advantage of the GPU many-core technology to speedup monitoring and reduce the runtime overhead.

Architecture

architecture overviewSource code and download

RiTHM's source code can be downloaded via the following link.

RiTHM's Source Code

The source code is also available at the BitBucket repository:

RiTHM's BitBucket source

To clone the repository, go to the dedicated local directory and run the following command:

git clone https://[username]@bitbucket.org/embedded_software_group/rvtool.git

Resources

RiTHM's user guide can be downloaded from the following link. This user guide contains the installation instructions along with the prerequisites, and how to run and use RiTHM.

User Guide

Two screencast demos  can also be found here:

  • Monitoring with fixed polling period
Watch video on YouTube
  • Control-theoretic monitoring with dynamic polling period
Watch video on YouTube

A tool paper describing RiTHM's features can be found here.

The wikipage of the back-end verifier GooMF can be found here:

GooMF wiki

Related publications

For related publications, see the page on time-triggered runtime verification.

Contact

To report problems or ask questions about installation or execution of the tool, please email Yogi Joshi. For all other inquiries, please contact Prof. Borzoo Bonakdarpour.

Project members: 
Shay Berkovich
Graduate student
Samaneh Navabpour
Graduate student
Johnson Thomas
Graduate student
Wallace Wu
Graduate student
Yogi Joshi
Graduate student
Last updated: July 18, 2014

Related Publications

Medhat, R., B. Bonakdarpour, and S. Fischmeister, "Power-efficient Multiple Producer-Consumer", IEEE 28th International Symposium on Parallel & Distributed Processing (IPDPS), Phoenix, USA, pp. 669--678, 2014. PDF icon [paper] (680.49 KB)
Berkovich, S., B. Bonakdarpour, and S. Fischmeister, "GPU-based Runtime Verification", IEEE International Parallel & Distributed Processing Symposium (IPDPS), May, 2013. PDF icon [paper] (388.53 KB)
Wu, W., D. Kumar, B. Bonakdarpour, and S. Fischmeister, "Reducing Monitoring Overhead by Integrating Event- and Time-triggered Techniques", Proc. of the International Conference on Runtime Verification (RV), Sept, 2013. PDF icon [paper] (1.18 MB)
Navabpour, S., Y. Joshi, C. Wah Wallace, S. Berkovich, R. Medhat, B. Bonakdarpour, and S. Fischmeister, "RiTHM: A Tool for Enabling Time-triggered Runtime Verification for C Programs", Proc. of the ACM Symposium on the Foundations of Software Engineering (FSE), St. Petersburg, Russia, 2013.
Navabpour, S., B. Bonakdarpour, and S. Fischmeister, "Path-aware Time-triggered Runtime Verification", Third International Conference on Runtime Verification (RV), Istanbul, Turkey, pp. 199-213, September, 2012. PDF icon [paper] (509.83 KB)
Bonakdarpour, B., J. Thomas, and S. Fischmeister, "Time-triggered Program Self-monitoring", Proc. of 18th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Seoul, Korea, pp. 260-269, 2012. PDF icon [paper] (377.34 KB)
Medhat, R., B. Bonakdarpour, D. Kumar, and S. Fischmeister, "Runtime Monitoring of Cyber-Physical Systems Under Timing and Memory Constraints", ACM Transactions on Embedded Computing Systems (TECS), vol. 14, issue 4, pp. 79, 2015.
Berkovich, S., B. Bonakdarpour, and S. Fischmeister, "Runtime Verification with Minimal Intrusion Through Parallelism", Formal Methods in System Design, pp. 1-32, 2015.
Bonakdarpour, B., S. Navabpour, and S. Fischmeister, "Time-triggered Runtime Verification", Formal Methods in System Design (FMSD), vol. 43, issue 1, pp. 29--60, 2013. PDF icon [paper] (2.95 MB)