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 4 articles )
Showing results 1 to 4 of 4.
- Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
- Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan: A compiler for MSVL and its applications (2018)
- 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)