Hardware Reference
In-Depth Information
16.2
Solving Testing in Context Via Language Equations
We use the parallel composition operator to illustrate solving testing in context
by equation solving, but all the results hold also for the synchronous composition
operator.
We consider the parallel composition of two communicating FSMs, the context
FSM
Context
DhS
Context
;I [ V; O [ U; T
Context
;r
Context
i
and the embedded FSM
Emb
DhS
Emb
;U;V;T
Emb
;r
Emb
i
, as shown in Fig.
16.1
. The alphabets
I
and
O
represent the
external
inputs and outputs of the system, while the alphabets
V
and
U
represent the
internal
interactions between the two machines. For the
sake of simplicity, we assume that all communicating machines are complete and
deterministic. The external behavior of the composition is given by the complete
deterministic FSM
Spec
def
D
Context
˘
Emb
defined over external input and output
alphabets
I
and
O
.
Given an implementation of the topology in Fig.
16.1
, suppose that the imple-
mentation of the FSM
Context
is fault-free, and that we would like to generate
tests in order to check whether the FSM
Emb
is correctly implemented, i.e., the
composition of
Context
and
Imp
,where
Imp
is the implementation of
Emb
,hasthe
same behavior as the FSM
Spec
. Here, for solving the problem we use two test
suites. An
internal test suite TS
int
is a finite set of finite internal input sequences,
while an
external test suite TS
ext
is a finite set of finite external input sequences.
An FSM
Imp
is
externally distinguishable
from
Emb
or distinguishable from
Emb
composed with
Context
, if there exists an input sequence such that the FSMs
Spec
and
Context
˘
Imp
have different output responses to such input sequence. We
know that the equivalence of
Context
˘
Emb
and
Context
˘
Imp
does not imply the
equivalence of
Emb
and
Imp
, i.e., non-equivalence in the context is weaker than non-
equivalence in isolation due to the lack of controllability and observability [114]. It
I
Context
O
U
V
Emb
Fig. 16.1
Topology of
parallel composition of two
FSMs used for testing in
context
Spec
Search WWH ::
Custom Search