Information Technology Reference
In-Depth Information
a theorem on (timed) trace renement whose interpretation below indicates how
a useful TASL should be constructed:
Theorem 2.
Let specSUT be an abstract specication process of the desired
SUT behaviour. Let impSUT denote the SUT implementation and ENV the
environment (including the TASL) used for testing. Then, if
ENV
0
(
ENV
k
specSUT
)
v
T
(
ENV
k
impSUT
)
and ENV
v
T
holds,
(
ENV
0
k
(
ENV
0
k
specSUT
)
v
T
impSUT
)
follows.
traces
(
ENV
0
k
Proof.
Let
s
2
impSUT
). This implies
:
2
traces
(
ENV
0
)
\
k
1
s
traces
(
impSUT
)
[semantics of
]
ENV
0
]
:
2
v
T
2
s
traces
(
ENV
)
[
ENV
3
:
s
2
traces
(
ENV
k
impSUT
)
[semantics of
k
]
4
:
s
2
traces
(
ENV
k
specSUT
)[
ENV
k
specSUT
)
v
T
(
ENV
k
impSUT
)]
5
:
s
2
traces
(
specSUT
)
[semantics of
k
]
traces
(
ENV
0
)
6
:
s
2
\
traces
(
specSUT
)
[1. and 5.]
traces
(
ENV
0
k
7
:
s
2
specSUT
)
[semantics of
k
]
(
ENV
0
k
(
ENV
0
k
8
:
specSUT
)
v
T
impSUT
)
[Denition of (timed) trace renement.]
t
In the context of FTC testing,
specSUT
denotes the specication of the
system under test,
impSUT
denotes its implementation
8
and
ENV
denotes the
test environment consisting of the operational FTC environment plus the TASL
residing in the FTC application layer. Let
ENV
0
denote a concrete operational
environment plus concrete application layer. Since the operational environment
is modelled equivalently in the test environment, the relation
ENV
v
T
ENV
0
will hold if the concrete application layer is a renement of the TASL. From the
underlying testing theory we know that successful exhaustive testing according to
the test strategy implemented in
RT-Tester
would imply the renement relation
(
ENV
impSUT
) (see [21,22]). Now the theorem above
may be interpreted as follows: suppose that an exhaustive test suite has been
successfully executed in the test environment
ENV
. Further suppose that the
TASL has been designed in such a way that it is rened by every concrete
application layer. Then the behaviour of the FTC operating in any concrete
environment plus application layer
ENV
0
will be a renement of its associated
specication (
ENV
0
k
k
specSUT
)
v
T
(
ENV
k
specSUT
).
The last question to be solved is how to specify and construct a TASL satisfy-
ing the above mentioned property. Now the most general admissible behaviour of
8
Of course, the explicit formal representation of
impSUT
is unknown, but its existence
is guaranteed.
Search WWH ::
Custom Search