Skip to main content

RiTHM: A Tool for Enabling Time-triggered Runtime Verification for C Programs

Publication Type
Year of Publication
2013
Conference/Journal Name
ACM Symposium on the Foundations of Software Engineering (FSE)
Publisher
ACM
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.