Frequently Asked QuestionsWhat is runtime verification?
Runtime verification is a computing system analysis and execution approach where data is collected
during the concrete or symbolic execution of programs and used to react to behaviors
that satisfy certain properties. These properties can model either correct or incorrect behaviors of the program, allowing
for a higher degree of confidence in the correct operation of the system, by triggering the execution of recovery code during deployment or
finding bugs before deployment or both. Runtime verification techniques are strongly based
in formal program reasoning and analysis, and provide rigorous guarantees about the correctness of a system's operation.
Runtime verification based techniques (and indeed software developed at Runtime Verification, Inc.) has been used to find
bugs in widely used production software.
Runtime verification is not just testing. It can find bugs dynamically, but it is a lot more than that. It is after all
a verification approach, allowing you to eventually verify programs, proving them correct. However, the RV approach is new and,
unlike static analysis, a bit unconventional. It starts from executing the actual program you want to verify, and stretches from there,
encompassing
prediction, symbolic execution, and eventually even full verification by exhaustive symbolic execution. Different tools specialize on
different such features,
and the more time you spend testing/executing, the more you cover. You can even use RV tools as a methodology to write correct programs
and/or prove them correct.
What is a property and how do I write one?
A property is just a formal expression of something in the system you would like to check or enforce. It could be the order in which certain method calls occur, the required state of the environment for certain actions to occur, the conditions in which a global variable can be accessed, or any other expression of the desirable or undesirable behavior of a system. The most common way to obtain properties is to simply use properties prepackaged by Runtime Verification Inc. We have already formalized a large portion of the Java API, developed properties for concurrency violation detection, and much more. See the web documentation of each of our products to see how to use prepackaged or predeveloped properties, as well as for information on how to develop new and custom properties.
How can runtime verification recover from errors?
When a property is detected as being violated or satisfied, runtime verification allows for arbitrary code to be executed. Together with the information about program state gleaned from the property itself, this can allow for corrective code to ensure the safety of the system or even prevent the property itself from being violated. For example, suppose that your property is "never use a resource before authentication". You can write the property so that RV-Monitor triggers the property violation when the function use_resource() is called, that is, before the code actually using the resource is executed. This way, nothing catastrophic has happened when this event occurs. Moreover, you can tell RV-Monitor to execute the function authenticate() when the violation takes place and this way you now got a provably correct system without ever even touching its code! RV-Monitor observed the execution and steered it to satisfy the property.
Isn't runtime verification resource intensive or slow?
Using over 200 properties, RV-Monitor has been shown experimentally to have approximately a 10-20% overhead on reasonable sized programs. This means that if your program runs in 100 seconds, you will only have to wait 20 additional seconds to run with the verification of over 200 properties. RV-Predict requires slightly more resources, applying a predictive algorithm to determine property violations that may not have occured. RV-Match is our most resource intensive tool, executing a program symbolically along all its possible execution paths. This is a resource intensive process, but represents the most thorough possible check of a program's behavior.
Doesn't runtime verification consider only one possible execution?
While this is true for some traditional runtime verification techniques, this does not hold for all of our products. RV-Predict is able to predict even unobserved concurrency violations from the execution trace, while RV-Match explores all possible executions of a program symbolically using the programming language's formal semantics. While RV-Monitor does only enforce and verify problems for a given execution, this is a design choice that allows RV-Monitor to have a low overhead and thus be run across a vast number of executions, or even continuously in production.
