kirancodes.me
To Proof Maintenance & Beyond!
FSE 2013

RiTHM: a tool for enabling time-triggered runtime verification for C programs

Samaneh Navabpour, Yogi Joshi, Chun Wah Wallace Wu, Shay Berkovich, Ramy Medhat, Borzoo Bonakdarpour, Sebastian Fischmeister

PDFDOI 10.1145/2491411.2494596dblp

Abstract

We introduce the tool RiTHM (Runtime Time-triggered Heterogeneous Monitoring). 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. RiTHM provides two techniques based on static analysis and control theory to minimize instrumentation of the input C program and monitoring intervention. The monitor's verification decision procedure is sound and complete and exploits the GPU many-core technology to speedup and encapsulate monitoring tasks.

BibTeX
@inproceedings{Navabpour-al:FSE13,
  author    = {Samaneh Navabpour and
               Yogi Joshi and
               Chun Wah Wallace Wu and
               Shay Berkovich and
               Ramy Medhat and
               Borzoo Bonakdarpour and
               Sebastian Fischmeister},
  title     = {{RiTHM:} a tool for enabling time-triggered runtime verification for C programs},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {603--606},
  publisher = {{ACM}},
  year      = {2013},
}

Related papers