This post is meant to be the first in a series of blog posts about Runtime Verification.
Disclaimers
Runtime Verification, also referred to as Runtime Monitoring, is a broad term that means different things to different people. Additionally, there are various Runtime Verification systems and paradigms. In this blog post I will be referring to Runtime Verification a la the JavaMOP framework (paper, Github) and its usage with Java unit tests, where my expertise in the area primarily comes from.
What is Runtime Verification (RV)?
Runtime Verification (RV) is a dynamic program analysis that checks program executions against formally specified properties. In other words, RV involves running a program, and checking information about that execution against specifications on things you want to have always true (or false) about your program. If a specification is violated, then it means that your property was not held by your program, implying the discovery of a bug.
To draw this out in a diagram...
In a normal program execution, our program takes in an input and produces an output. But, we don't necessarily know what is happening in the program itself. We can use debuggers, printf debugging, or logging to obtain information about program state, but we don't necessarily have a quick way to discern whether the process (i.e. the series of steps) is correct. Because of this, in normal program execution, we consider the program itself as a black box.
However, RV offers a way to probe the black box, and "see" the internals of the program process. RV can be considered a wrapper around your program execution. It takes in a specification(s) written in formalisms such as Linear Temporal Logic. The specifications establish properties that you want your program to abide by. For example, a specification may say that a setup() function always ought to be called before a process() function. RV takes in these properties, and produces monitors, labeled with "M" in the diagram. These monitors are extra functions that attach themselves to definitions of the functions of interest. During runtime, the monitors will check whether the specification is held true. If a monitor detects that a specification was violated, for example process() was called without a preceding call to setup(), then it fires a violation, which indicates the location of code where the specification was violated.
Some technicalities:
- RV is called Runtime Verification because of the principle that a RV system can help the subject execution recover from violations that it discovers. When an execution recovers from a buggy state, it would be "correct", hence the system "verifies" the correctness of the execution. In practice, when a violation occurs, an alarm is raised to indicate to the user the location of a likely bug. But, all of this is up to the user and the specifications they pass to the RV system.
- In JavaMOP, the analysis will be done while the program is running (called online monitoring), but there are also variants of RV that output execution information to logs and do the checking separately (called offline monitoring).
Why Runtime Verification?
Establishing the correctness of your program is no easy task. Often times when we write a piece of code and see that "it works", all that it means is that we have a hightened confidence in our program. Most likely, there are still bugs hiding in the background.
Runtime Verification sits in a sweet spot where it can offer some formal guarantees, while also having the flexibility to apply to more number of, and bigger programs. Two other prevalent ways to assess correctness of a program are Formal Verification and Testing. On one hand, formally verifying your code involves constructing a mathematical proof of the correctness of your program. This is the closest to being absolutely sure that your program is correct, but it also involves an expensive process and building background in theorem proving tools. On the other hand, we can test our program by feeding inputs and comparing outputs with expected ones. Testing is relatively less difficult than formally verifying, since we only have to consider the inputs and outputs. We also have testing frameworks and automatic test generators that can help us run and write tests for many programs. But testing never proves correctness (without giving infinite inputs and outputs, which we cannot do), and we only see the end points of our program. Due to its ease, testing is the de-facto standard way of quality assurance/correctness checking, but what if we still wanted more formal guarantees about our code?
In Runtime Verification, you provide a set of specifications, which can reason about the internals of your program, not just the input and output. Since it's a dynamic analysis, it will only apply to one execution at a time and hence not give you the full guarantees that formal verification does. But, you get more guarantees about the correctness of your program than simply testing does. A violation can also be more helpful than a failing test since it indicates the precise location of code where the specification was violated.