Information Technology Reference
In-Depth Information
measured values are put into a buffer. Before the next iteration starts, the
trace is extended accordingly. A checking iteration consists of two steps:
-
Evaluation Phase
:Inthe
evaluation phase
all subformulas and all states
from a start state up to an
end state
are sequentially computed. The
end state is determined by the largest time instant for which a value for
all attributes exists. For states beyond this last state the extrapolated
interval, as explained above, is used. The evaluated area will be called
frame.
The start state for the next checking iteration is the last checked
state.
-
Refinement Phase:
The evaluation of the last frame results in new in-
formation of attribute behaviours. States already evaluated in previous
iterations can thus be refined. This is done by backward iterating all
previously evaluated states until no further refinement on values can be
performed.
The evaluation of temporal operators is realized according to their recursive
characterizations. In the following, the idea of the procedure is shown for the
always
operator. Let
T
be an (extrapolated) trace,
v
be an attribute and
i
∈
N
a time instant. The evaluation of
v
at time
i
then is denoted by
∀
i
∈
N
:
T
ϕ
(
i
)=
T
ϕ
(
i
)
∧
T
ϕ
(
i
+1)
.
(5)
In order to be able to compute the formula values correctly, we store the cur-
rent evaluation results for all time instants of all attributes and subformulas.
That this information is needed becomes clear when one considers how to
evaluate formulas with nested temporal operators like
.
The refinement phase concerns the update of these preliminary values, re-
flecting the effect of tightening intervals extrapolated previously. Note that
the final result is the evaluation of the topmost formula operator in the first
state.
The idea of the refinement process is shown in the example of Fig. 2: In
the figure, the truth values starting from state
j
up to state
endState
of
both formulas,
f
1
=
♦(
a>c
1
)
U
(
b>c
2
)
ϕ
are depicted. The left part of the figure
illustrates the result after the evaluation phase for the shaded area. The
effect of the subsequent refinement phase is demonstrated in the right part
of the figure, leading to tighter intervals up to state
traceRefinedUpTo
.
The information about changed values of subformulas during refinement is of
course important for the refinement of the enclosing formula.
An exact evaluation of formulas according to the procedure sketched above
is rather costly. In order to reduce the state space, one can merge multiple
measured values into one if they are very similar, e.g., their values only dif-
fer by a fixed threshold. In practice, this has been proven to be very useful,
as measurements arrive with a very high frequency while the corresponding
values do only differ slightly. To illustrate the effects of such merging tech-
niques, we have specified and evaluated different formulas which refer to the
attributes of the car in our application scenario. The results are illustrated
ϕ
and
f
2
=
