RiTHM: a tool for enabling time-triggered runtime verification for c programs. 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.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Berkovich, Shay; Bonakdarpour, Borzoo; Fischmeister, Sebastian: Runtime verification with minimal intrusion through parallelism (2015)