RV: A Runtime Verification Framework for Monitoring, Prediction and Mining
Grigore Rosu
University of Illinois at Urbana-Champaign (UIUC)

Runtime verification is an emerging approach which consists of

1. observing the execution of the target system,
2. checking the observed execution trace against the requirements, and
3. steering the running program to avoid catastrophic failures if needed.

Runtime verification avoids the complexity of full-blown formal verification by analyzing a model extracted from the execution of the program rather than from the program itself. It also avoids the ad hoc nature of testing by taking formal specifications and analyzing models (extracted from traces) which may be more complex than linear sequences of events. The current limitations of runtime verification are the following:

1. runtime and memory overhead - to observe a program one needs to instrument it and to manage a potentially unbounded number the monitors;
2. limited coverage - there could be errors in the program which are not encountered in the observed execution trace; and
3. need for formal specifications - to state the correctness criteria, one still needs to provide formal specifications.

RV is a runtime verification framework currently under development by a startup company jointly with the Formal Systems Laboratory at UIUC.

The objective of RV is to circumvent the current limitations of runtime verification. The runtime and memory overhead are addressed by developing efficient instrumentation and monitor garbage collection.The limited coverage is addressed by extracting causal models from execution traces and analyzing them efficiently; this way, a causal model may predict an error in the running system even though the error has not been hit during the observed execution. Finally, to relieve users from writing formal specifications, an automated specification miner observes execution traces and learns the most likely formal specifications that they obey. The ultimate goal of RV is to not only allow its users to employ monitoring, prediction and mining in their systems, but also to combine them in ingenious ways. For example, one can completely automatically mine likely specifications and then use prediction on them to detect potential errors. Or one can mine properties of a library using traces from trusted programs, and then use the mined properties to monitor or predict errors in untrusted programs.

RV extends and combines technologies developed under the UIUC projects JavaMOP (OOPSLA'07, TACAS'09, PLDI'11), jPredictor (CAV'07, ICSE'08) and jMiner (ICSE'11).