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.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Kassem, Ali; Falcone, Yliès; Lafourcade, Pascal: Formal analysis and offline monitoring of electronic exams (2017)
- Berkovich, Shay; Bonakdarpour, Borzoo; Fischmeister, Sebastian: Runtime verification with minimal intrusion through parallelism (2015)