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.
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
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
A tool paper describing RiTHM's features can be found here.
The wikipage of the back-end verifier GooMF can be found here:
For related publications, see the page on time-triggered runtime verification.