Information Technology Reference
In-Depth Information
specification by adding quiescence (
δ
) self loops in states where no output event
is observable. Such states are called quiescent states. The purpose of quiescence
is to exploit the absence of any observable events as an observation itself. Quies-
cence is realized as timeout event, i.e., if the implementation does not send any
output within a specified timeout then
δ
can be observed. Thus, the timeout as-
sociated with
δ
has to be greater than the maximum response time of all other
output events in the system. In Example 2, we discuss how the observation of qui-
escence can be employed to resolve decision conflicts during synchronous testing.
Such conflicts arise in states where the tester has the choice between either apply-
ing an input or observing outputs. After adding
δ
self loops in quiescent states,
determinization is applied resulting in the suspension automaton.
Environmental changes in qualitative action systems are designated by
qual
events. These events mark the firing of the qualitative action. If a tester's choice
depends on a previous environmental update, such
qual
events have to be ob-
servable by the tester. Referring to our running example, a tester's input to the
system is the controllable
WATER REQ(X)
event, where
X
is a Boolean param-
eter for requesting water or not. Note that the guard of this input action depends
on the water level of tank
T
2. Hence, we have to declare qualitative evolutions
as observable events. Otherwise, the nondeterminism of the model would pre-
vent the enabledness of the controllable action according to the controllability
condition (4), discussed in section 5.3.
Example 1.
Figure 7 shows a part of the conformance verification result between
the system specification and a mutant. In the mutant, the action
PUMP1 OFF
:
g
2
→
p1 running
:=
true
;
inout
:= (0
,
0)
has been modified such that the Boolean flag denoting the state of pump
P
1
remains
true
although it should be set to
false
.The
ctr
prefix of actions means
that the action is controlled by a tester while
obs
denote observations a tester
can make from the implementation. As can be seen in Figure 7, the mutation is
revealed when the tester tries to turn off pump
P
1 twice which is in difference
to the specified behavior. After unexpected output behavior, not permitted by
the specification,
fail
states are appended in the product LTS. The behavior of a
mutant following after
pass
states is allowed by the
ioco
relation. Furthermore,
the parametric values of
qual
events denote the environmental condition at the
end of an evolution. For example, the first evolution after the initial state fills
the lower tank to the
Ful l
level and the upper tank remains empty. Then pump
P
1 is turned on which subsequently causes another evolution filling the upper
tank
T
2. Here, depending on the flow rates and tank volumes several outcomes
are possible.
Applying the conformance verification step to several different mutants yields
the results shown in Table 2. In the first column
ASO
stands for the
Associa-
tion Shift Operator
which changes the association between variables in Boolean
expressions.
ENO
is the shorthand for the
Expression Negation Operator
,
ERO
