Databases Reference
In-Depth Information
on the characterization of intermediate (inner) states, merging them may be
an attractive option to accelerate convergence without undue precision loss.
Example 6.4.8. Figure 6.6 presents abstract histories produced during the
analysis of the single instance key in our running example, using the 1-past
abstraction with exterior merge. The first row describes the histories observed
at the end of the first iteration of the
for
loop of
example()
, in which a channel
is connected, and either the
receive
procedure, reading bytes from the channel,
or the
send
procedure, writing bytes on the channel, is invoked. These all hold
abstract histories for the same instance key at the same abstract state. Each
history tracks a possible execution path of the abstract object.
Although these histories refer to the same instance key and alias context,
exterior merge does not apply since their current states are not equivalent.
The second row shows the result of applying the extend transformer on each
history after observing a
connect
event at the beginning of the next iteration
of the
for
loop. The intermediate step, before the quotient construction, for
the automaton on the left is depicted in Figure 6.8(a). There, and in all other
cases as well, the new state is equivalent to an existing state according to the
1-past relation; a state with
connect
as its incoming event already exists in
each automaton. As a result, extend simply adds the new transitions and adds
no new states.
After observing this event, the resulting three histories meet the exterior
merge criterion, and are therefore combined. The analysis discards the original
histories and proceeds with the merged one which overapproximates them.
Figure 6.7 presents the corresponding abstract histories using the 1-future
abstraction with exterior merge (in fact, in this case total merge behaves iden-
tically). Unlike the case under the past abstraction, merge applies at the end of
the first loop iteration, since the initial and current states are equivalent under
the 1-future relation. As a result, the analysis continues with the single merged
history. The second row shows the result of applying the extend transformer
on it after observing a
connect
event.
Figure 6.8(b) presents the intermediate step in which the merged abstract
history is extended by
connect
, before the quotient is constructed. An outgoing
transition labeled
connect
is added from state 5 (the previous current state)
to a new state, making state 5 share a future with state 1. Thus states 1 and
5 are merged, resulting in the abstract history depicted in the second row of
Figure 6.7.
Nondeterminism. It is easy to verify that the quotient structure of a deter-
ministic automaton w.r.t. R
k
past
is deterministic. This ensures that the k-past
abstraction always produces deterministic automata, as demonstrated by Fig-
ure 6.6. On the other hand, when the future parameter is nontrivial (i.e.,
k
2
6= 0), nondeterminism can result during the quotient construction. For
example, in Figure 6.7, all the automata are non-deterministic.
Precision. If automata satisfy the following structural property, then we can
prove that the past-future abstraction is precise.
Search WWH ::
Custom Search