MOP: A Generic and Efficient Runtime Verification Framework

We present a tool-supported formal software development framework in which runtime monitoring is a basic design principle, called monitoring-oriented programming (MOP). In MOP, the developer specifies desired properties using definable formalisms, along with code to execute when properties are violated or validated. MOP automatically generates monitors from the specified properties and integrates them together with the user-defined code into the original system. We show that, despite its genericity with respect to specification formalisms, our MOP implementation for Java adds less runtime overhead than other exiting runtime verification systems with hardwired specification formalisms: for example, MOP’s runtime overhead was larger than 10% in fewer than 8% of the programs in the DaCapo benchmark.

When used for detecting errors in concurrent systems, runtime monitoring in general and MOP in particular suffer from the same limited coverage as testing. We also present a predictive runtime analysis technique that significantly increases the analysis coverage of monitoring in the context of bug-detection in multithreaded systems, having at its core an improved happen-before causality sliced using static analysis.

MOP Webpage: http://fsl.cs.uiuc.edu/mop