Runtime verification

From Wikipedia, the free encyclopedia

Runtime verification is a verification technique that combines formal verification and program execution. It is the process of detecting faults in a system under scrutiny by passively observing its input/output behavior during its normal operations. The observed behavior, e.g., in terms of log traces, of the target system can be monitored and verified dynamically to satisfy given requirements. Such requirements are typically specified by a formalism which can express temporal constraints, such as LTL-formulae (Linear temporal logic) or automata and statecharts. In contrast to the classical model checking approach, where a simplified model of the target system is verified, runtime verification is performed while the real system is running. Thus, runtime verification or as it is sometimes referred to, passive testing, increases the confidence on whether the implementation conforms to its specification. Furthermore, it allows a running system to reflect on its own behavior in order to detect its own deviation from the prespecified behavior.

In contrast to other formal verification methods such as model checking, runtime verification has to deal with finite traces only, as at an arbitrary point in time the system will be stopped and so its execution trace. The exception to this rule is a deployed runtime monitor that monitors on a potentially never ending deployed application for the purpose of detecting requirement violations while the application is running. To this end the formal specification must contain a recovery specification.

Continuous monitoring of the runtime behavior of a system can improve our confidence in the system by ensuring that the current execution is consistent with its requirements at runtime. In the literature, at least the following four reasons are mentioned in order to argue for runtime verification:

If you check the model of your system you cannot be confident on the implementation since correctness of the model does not imply correctness of the implementation.

Some information is available only at runtime or is convenient to be checked at runtime.

Behavior may depend heavily on the environment of the target system; then it is not possible to obtain the information necessary to test the system.

In the case of systems where security is important or in the case of critical systems, it is useful also to monitor behavior or properties that have been statically proved or tested.

Another good reason to use runtime verification is that it allows for formal specification and verification or testing of the properties that a system has imperatively to satisfy. Traditional testing techniques such as unit testing are ad hoc and informal. It is only a partial proof of correctness in that it does not guarantee that the system will operate as expected under untested inputs. In terms of its ability to guarantee software correctness, runtime verification is weaker than formal methods but stronger than testing. Testing can only guarantee the correctness of a limited set of inputs at implementation time. As a result, undiscovered faults may result in failures at runtime, and even allowing the system to propagate corrupted output because the failure was not detected. By always monitoring the software for correctness, such failures can be caught when they happen, for any input which causes them to occur. However, runtime verification is weaker than formal methods because such guarantees can not be made a priori.