Hardware Reference
In-Depth Information
a
b
i
2
/
u
1
u
1
/
v
2
v
2
/
u
1
q
0
q
1
t
0
t
1
u
1
/
v
1
i
2
/
o
2
u
2
/
v
1
v
2
/
o
2
i
1
/
u
2
v
1
/
o
1
v
2
/
v
1
i
1
/
u
1
v
2
/
u
2
c
d
u
2
/
v
1
i
1
/
o
1
u
1
/
v
1
i
1
/
o
1
u
1
/
v
2
s
0
s
2
p
1
p
2
p
3
u
1
/
v
2
i
2
/
o
2
u
1
/
v
1
i
2
/
o
1
u
2
/
v
1
u
2
/
−
u
2
/
v
2
i
2
/
o
2
u
1
/
−
u
2
/
v
1
dc
p
5
p
4
s
1
u
2
/
v
2
i
1
/
o
2
−
/
−
u
2
/
−
(
a
) FSM
Context
;(
b
) FSM
Emb
;(
c
) FSM
Spec
def
Fig. 16.2
D
Context
˘
Emb
;(
d
) Largest solution
of the equation
Context
˘ X Š
Spec
that is externally distinguishable from
Emb
, there exists a sequence in
TS
int
that
distinguishes
Imp
and
Emb
. The subset of
J
Emb
that contains FSMs externally
indistinguishable from
Emb
is characterized by the FSM
Largest
, therefore, the
problem of generating a complete internal test suite becomes now as follows. Given
the pair
J
Emb
and
Largest
, we are required to determine a set
TS
int
of input sequences
such that for each FSM
Imp
2 J
Emb
that is not a reduction of the FSM
Largest
,
there exists
˛ 2
TS
int
such that the output response of
Imp
under the input
˛
cannot be produced by the FSM
Largest
under
˛
. This problem can be solved
using the method developed in [108] for generating complete test suites for the
case of reduction relation between implementation and specification FSMs. Such
a complete internal test suite can be translated into a complete external test suite
according to Proposition
16.2
.
We illustrate the approach for testing an embedded component using an example
from [114].
Example 16.3.
Given the topology in Fig.
16.1
, consider the instances of
Context
,
Emb
and
Spec
in Fig.
16.2
a-c; the largest complete solution of the equation
Context
˘
X
Š
Spec
is shown in Fig.
16.2
d. FSM
Emb
is included in
Largest
,
Search WWH ::
Custom Search