@article{67,
  keywords = {Formal methods, Parallel algorithms, Runtime monitoring, Temporal logic},
  author = {Shay Berkovich and Borzoo Bonakdarpour and Sebastian Fischmeister},
  title = {Runtime Verification with Minimal Intrusion Through Parallelism},
  abstract = {<p>Runtime verification is a monitoring technique to gain assurance about well-being of a program at run time. Most existing approaches use sequential monitors; i.e., when the state of the program with respect to an event of interest changes, the monitor interrupts the program execution, evaluates a set of logical properties, and finally resumes the program execution. In this paper, we propose a GPU-based method for design and implementation of monitors that enjoy two levels of parallelism: the monitor (1) works along with the program in parallel, and (2) evaluates a set of properties in a parallel fashion as well. Our parallel monitoring algorithms effectively exploit the many-core platform available in the GPU. In addition to parallel processing, our approach benefits from a true separation of monitoring and functional concerns, as it isolates the monitor in the GPU. Thus, our monitoring approach incurs minimal intrusion, as executing monitoring tasks take place in a different computing hardware from execution of the program under inspection. Our method is fully implemented for parametric and non-parametric 3-valued linear temporal logic. Our experimental results show significant reduction in monitoring overhead, monitoring interference, and power consumption due to leveraging the GPU technology. In particular, we observe that our parallel verification algorithms are indeed scalable.</p>
},
  year = {2015},
  journal = {Formal Methods in System Design},
  pages = {1-32},
  issn = {0925-9856},
  doi = {10.1007/s10703-015-0226-3},
}