Accelerated Runtime Verification of LTL Specifications with Counting Semantics

Runtime verification is an effective automated method for specification-based offline testing and analysis as well as on-line monitoring of complex systems. The specification lan-guage is often a variant of regular expressions or a popular temporal logic, such as Ltl. This paper presents a novel and efficient parallel algorithm for verifying a more expres-sive version of Ltl specifications that incorporates counting semantics, where nested quantifiers can be subject to nu-merical constraints. Such constraints are useful in evaluat-ing thresholds (e.g., expected uptime of a web server). The significance of this extension is that it enables us to reason about the correctness of a large class of systems, such as web servers, OS kernels, and network behavior, where properties are required to be instantiated for parameterized requests, kernel objects, network nodes, etc. Our algorithm uses the popular MapReduce architecture to split a program trace into variable-based clusters at run time. Each cluster is then mapped to its respective monitor instances, verified, and re-duced collectively on a multi-core CPU or the GPU. Our algorithm is fully implemented and we report very encour-aging experimental results, where the monitoring overhead is negligible on real-world data sets. 1