Information Technology Reference
In-Depth Information
5.3 Ensuring Controllability in Presence of Non-determinism
The
ioco
relation is a global property referring to la-
bel traces of the specification rather than to states
like simulation relations. This implies that the lo-
cal information in a certain state, in general, is
not enough to decide conformance. That is the
case for non-deterministic specifications where the
same trace leads to different states. Here the out-
puts of both states have to be considered by
ioco
which requires preceded determinization. Our
ioco
checker applies the computation of the suspension
automaton on-the-fly while computing the prod-
uct LTS of two given QAS. However, care has to
be taken during determinization regarding the en-
abledness of events. In action systems, events can
only occur if the action's enabledness guard is sat-
isfied in the current state. This guard is defined as
g
(
A
)=
df
¬
wp
(
A,
false
), ensuring that the action will
not terminate in an undefined post-state. Here,
wp
denotes the weakest precondition.
In the case of black-box testing, the state of a
system is internal and cannot be observed from
outside. If an action system model contains non-
determinism, i.e., internal actions and nondeter-
ministic updates, determinization of its labeled
transition system via subset construction leads to
sets of states. In the action system model, however,
for each of these states different subsequent events
(actions) could be enabled. Due to the abstraction
to an LTS we lose this information and in the LTS
the union of all enabled events would be indicated
as valid subsequent actions. This information loss
leads to a problem during test case execution, as the implementation might
make another internal decision than the test driver. In the end, the tester might
not know in which state the SUT is in and worse, which events are allowed. Be-
cause we require the SUT to be input-enabled, the tester might not even notice
the loss of synchronization immediately: the SUT has to ignore all inputs that
are not allowed. Of course, if the tester subsequently encounters an unexpected
observation, it would issue a fail verdict - which would be wrong in this case, as
the SUT made a valid internal choice.
To overcome this problem, we need to synchronize the test case execution
with the internal state decisions of the implementation. Since this is not possible
in blackbox testing, the alternative is to disallow input events with guards that
do not hold for all internal states. We denote the occurrence of an event
a
in
a state
s
as
s
a
Fig. 8.
An uncontrollable
two-tank system caused by
too coarse observations
→
. The following property states that an action from the set of
