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.
What products does Runtime Verification Inc. currently offer?
Runtime Verification Inc. is currently developing three core products: RV-Predict is a predictive runtime analysis tool focused on automatically detecting concurrency errors in your programs. RV-Monitor is a development methodology and library generation tool allowing for the monitoring and enforcement of user-selected properties at runtime. RV-Match is a tool allowing for exhaustive runtime verification to be performed symbolically on all possible program paths, proving certain properties correct for all possible executions of a given program.
When and why should I use RV-Predict?
RV-Predict should be used any time concurrency correctness is important to a multithreaded application. RV-Predict is able to efficiently and seamlessly detect concurrency issues and data races in programs, is very easy to run, and generally requires no configuration whatsoever. RV-Predict also leverages unique predictive capabilities to detect possible races even if they do not occur in the execution trace recorded by RV-Predict.
When and why should I use RV-Monitor?
RV-Monitor allows for the monitoring of complex applications or systems and the enforcement of properties over their execution traces. RV-Monitor should be used whenever a specification exists by which the development of a program is governed, and adherence to the specification is a critical feature of the software. RV-Monitor can also be used to monitor compliance to generic APIs, including the Android and Java APIs.
When and why should I use RV-Match?
While RV-Monitor can verify and enforce compliance to certain properties for a given execution of a program, RV-Match can prove the correctness of a program at runtime, analyzing the execution trace on all possible execution paths and over all possible inputs. RV-Match provides strong correctness guarantees, leveraging a formally defined semantics of the target language to simulate execution symbolically. RV-Match should be used when the strong guarantees of formal verification are desirable, and can also be used together with RV-Monitor to remove monitoring in areas where properties are provably never violated.
What is the development status of RV's products?
All of RV's products are currently open prototypes released for evaluation purposes. Development of all RV products is rapid and ongoing, so please check back soon for more changes as we approach release!
How can I buy a specific product?
Currently, there is no way to purchase programs and allow for commercial or non-academic use. If you are interested in using our technology in such a setting, please contact us using the page above.
What license covers Runtime Verification Inc.'s products?
There are two classes of project developed by RV: properietary products and projects licensed under an open license (as part of the RV open source ecosystem).
Proprietary products include all products not explicitly licensed under an open license, and are provided for evaluation and academic/noncommercial purposes only. Derivative works may not be created using proprietary RV products without first licensing them, and RV reserves all rights to proprietary products. Proprietary products may not be reverse engineered in any way.
Can I use proprietary RV products for academic use?
Yes! We welcome the use of RV's proprietary products in academic projects and research. If you are unsure as to whether you can include RV proprietary products in academic work, please use the contact page to contact us.
Can I use proprietary RV products for commercial use?
RV Products may not currently be used for commercial use. If you wish to license RV products for commercial use before we release official channels for purchasing our products, please contact us using our contact page.
Can I create derivatives of proprietary RV products?
Derivatives that include proprietary RV binaries are allowed only within the terms of the above license ( for academic and non-commercial evaluation purposes). You may not create derivatives using the source of any proprietary RV products without express written consent from Runtime Verification Inc.
