Information Technology Reference
In-Depth Information
This states that a property should only be evaluated to true or false, if any con-
tinuation of the execution will yield the same verdict. This ensures that runtime
verification is not stopped prematurely with the (misleading) understanding that
a property is violated or fulfilled although subsequent observations may yield a
different verdict.
The inconclusive verdict can be refined further to a verdict of presumably true
and presumably false . Presumably true expresses the fact that no violation has
been seen but one might still occur in the future as the observation might be
extended. Presumably false describes that some obligation is not satisfied but
might still be fulfilled in the future. These verdicts are of particular interest when
a system terminates as they still allow for some assessment where an inconclusive
verdict would have provided no information at all.
The maxim of impartiality can trivially be fulfilled with a monitor always
yielding the verdict inconclusive .Themaximof anticipation on the other hand
states that a verdict of true or false should be evaluated as soon as this is possible,
meaning for example for a violated safety property that the violation should be
reported by a monitor for the shortest execution of a run (i.e. the shorted prefix
of the run) violating the property.
The methods for checking properties of executions can broadly be divided into
rewriting-based and automata-based approaches. As described in [4], the latter
can sometimes be seen as pre-computations of rewriting-based approaches, high-
lighting that rewriting can be understood as on-the-fly automata constructions.
Thus, typically, rewriting-based approaches are easier to implement, may have a
better memory performance but may have a worse runtime performance. More-
over, anticipatory approaches to runtime verification need a complex check in
each verification step which can be done more e ciently using pre-computations
with automata.
A prominent specification formalism for denoting properties to check is Linear-
time Temporal Logic (LTL) [5], which allows to specify star-free regular prop-
erties. A bunch of different approaches for checking LTL properties at runtime
have been proposed. These can be categorized into two-valued rewriting-based
approaches [6,7,8], impartial three and four-valued rewriting and automata-
based approaches [9,4], or impartial and anticipatory automata-based approaches
[10,11]. The latter approach was then generalized to arbitrary linear-time tem-
poral logics which come with an automaton-based abstraction for a satisfiability
check in [12].
For practical applications, plain LTL specifications are typically not enough.
Besides enrichments like dealing with data or real-time aspects, one of the impor-
tant goals is to specify context-free properties, as, in software systems, nesting
structures arise naturally, in particular in the context of recursive programs
with calls and returns. State-full protocols impose nested structures on message
sequences. For example, a transaction protocol requires (recursively) any sub-
transactions of some transaction to finish before its completion. Similar prop-
erties arise in nested document formats such as XML or serialization of nested
data structures.
 
Search WWH ::




Custom Search