Information Technology Reference
In-Depth Information
Fig. 2. Refinement of the
always
operator. The shaded area is the last evaluated
frame. Left: Evaluation before refinement; Right: Evaluation after refinement.
real-time in order to provide the result timely. As mentioned in the previous
section we evaluate such formulas quantitatively. We face two main problems
in this evaluation process: First, the nature of the temporal operators requires
that in order to evaluate the truth value (or degree) at one time instant we
need the truth values of all future time instants. The second one is that the
semantics of such formulas are defined over infinite traces, so we have to find
a consistent interpretation on
finite
traces.
The first problem is solved in the manner that traces are safely extrapo-
lated for all future time instants. This is realized by interpreting attributes
over intervals rather than single values. For all time instants where a mea-
sured value for an attribute is already available we get a singleton interval.
If we have no further information about the evolution of an attribute, we
have to extrapolate its value for all time instants without measurements with
[
−∞
.
By annotating an attribute with a monotonicity information, a
tighter extrapolation can be performed: If an attribute is monotonically in-
creasing the last measured value is used as the lower bound for all future
time instants. For monotonically decreasing attributes the upper bound is
set analogously. Whenever new measurements are available, the values of
each previously evaluated time instant are refined.
The interval based evaluation also solves the above mentioned second
problem. At the end of each simulation run, the given formula
f
is evaluated
by an interval
,
∞
]
,
then all possible extensions of the observed trace will satisfy
f.
Analogously,
if
ub <
[
lb,ub
]
with
lb,ub
∈
N
which is interpreted as follows: If
lb >
0
then all extensions of the trace will not satisfy
f.
The evaluation
may result in an indefinite answer if the interval includes zero.
For our implementation it is crucial that the extrapolation for all future
time instants can be finitely represented. In the following, we sketch the
evaluation procedure.
The evaluation of a formula is realized bottom-up (wrt. the formula struc-
ture) and in a depth-first search manner (wrt. the states to be checked). The
online checking procedure is performed iteratively due to the evolving nature
of the trace. During a checking iteration the trace is not changed, i.e. newly
0
