Abstract: 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.

More on MOP http://fsl.cs.uiuc.edu/mop.

Grigore Rosu is an assistant professor at the University of Illinois at Urbana-Champaign (UIUC). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000 and his M.S. at the University of Bucharest, Romania, in 1996. He was offered the CAREER award by the NSF and the outstanding junior award by the Computer Science Department at UIUC in 2005. One of his papers won the best software science paper award at ETAPS 2002. Appointments: dcm@cs.cmu.edu