Runtime verification
Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties.
[1] Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically.
However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations [citation needed].
When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation.
Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis (because it avoids the tedious and error-prone step of formally modelling the system), at the expense of less coverage.
Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.
Checking formally or informally specified properties against executing systems or programs is an old topic (notable examples are dynamic typing in software, or fail-safe devices or watchdog timers in hardware), whose precise roots are hard to identify.
For large code bases, manually writing test cases turns out to be very time consuming.
Early contributions to automated verification were made at the NASA Ames Research Center by Klaus Havelund and Grigore Rosu to archive high safety standards in spacecraft, rovers and avionics technology.
[3] They proposed a tool to verify specifications in temporal logic and to detect race conditions and deadlocks in Java programs by analyzing single execution paths.
must hold for all parameter instances encountered (through parametric events) in the observed trace.
None of the following examples are specific to any particular runtime verification system, though support for parameters is obviously needed.
The figure to the right shows a finite-state machine that defines a possible monitor for checking and enforcing this property with runtime verification.
If, however, the hasNext() method returns false, there are no more elements, and the monitor enters the none state.
What follows is a representation of this property using parametric past time linear temporal logic.
The figure to the right shows Java code that matches this pattern, thus violating the property.
The SafeLock property enforces the policy that the number of acquires and releases of a (reentrant) Lock class are matched within a given method call.
This, of course, disallows release of Locks in methods other than the ones that acquire them, but this is very possibly a desirable goal for the tested system to achieve.
In the extreme, it is possible that there will be an instance of the property, i.e., a copy of the context-free parsing mechanism, for each possible combination of Thread with Lock; this happens, again, intuitively, because runtime verification systems may implement the same functionality differently.
Observing an executing system typically incurs some runtime overhead (hardware monitors may make an exception).
It is important to reduce the overhead of runtime verification tools as much as possible, particularly when the generated monitors are deployed with the system.
An additional inconvenience, particularly in the context of runtime verification, is that many existing specification languages are not expressive enough to capture the intended properties.
When the monitors are deployed with the system, instrumentation is typically minimal and the execution traces are as simple as possible to keep the runtime overhead low.
For example, augmenting events with Vector clock information and with data and control flow information allows the monitors to construct a causal model of the running system in which the observed execution was only one possible instance.
Any other permutation of events that is consistent with the model is a feasible execution of the system, which could happen under a different thread interleaving.
Unlike testing or exhaustive verification, runtime verification holds the promise to allow the system to recover from detected violations, through reconfiguration, micro-resets, or through finer intervention mechanisms sometimes referred to as tuning or steering.
Implementation of these techniques within the rigorous framework of runtime verification gives rise to additional challenges.
Many current runtime verification tools are hence built in the form of specification compilers, that take an expressive high-level specification as input and produce as output code written in some Aspect-oriented programming language (such as AspectJ).
The resulting sorting program is now more easily verifiable, the only thing being required from heap-sort is that it does not destroy the original elements regarded as a multiset, which is much easier to prove.
Techniques to increase the coverage of runtime verification for error detection purposes include:
