Personal tools

Run-time Verification

From PUMA Graduiertenkolleg

Jump to: navigation, search

Run-time verification tries to check correctness properties at run-time. Thus, run-time verification is complementary to static analysis methods. It is well-suited in cases where static analyzers may be too imprecise to infer the desired properties due to too coarse abstractions or to exceeding costs of their inference.

Run-time observation is typically based on correctness properties specified through temporal logic formulas which are translated into monitors which run in parallel to the original program and supervise the execution.

The use of monitors also simplifies testing of programs since test case generation may focus on the generation of program inputs and need not additionally deal with the prediction of corrrect program behavior. The latter is particularly difficult for real-time systems where small variations of exact time-points often are still acceptable.

On the other hand monitors staying within the code also beyond the testing phase may very well enforce, e.g., security guarantees also for program parts which have not been sufficiently tested or formally verified.

see "Máté Kovács"