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
Source
code
and
download
RiTHM's source code can be downloaded via the following link.
The source code is also available at the BitBucket repository:
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.
Two screencast demos can also be found here:
- Monitoring with fixed polling period
- Control-theoretic monitoring with dynamic polling period
Opportunities
Looking for motivated students (undergrads and grads) interested in working on embedded software and systems research. Mail Sebastian Fischmeister for further information.
A tool paper describing RiTHM's features can be found here.
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.
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.
Berkovich, S., B. Bonakdarpour, and S. Fischmeister, "GPU-based Runtime Verification", IEEE International Parallel & Distributed Processing Symposium (IPDPS), May, 2013.
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.
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.
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.
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.