Hardware Reference
In-Depth Information
and
V
(from the first fault domain). But it also contains FSMs which are not products
of the
Context
with any FSM. These are called “infeasible” machines in the sense
that they cannot be decomposed into the product of the
Context
and another FSM.
Problems
16.1.
Solve the FSM equation
M
A
˘ M
X
M
C
,where
M
A
is the context FSM
shown in Fig.
16.2
a, and
M
C
is the specification FSM in Fig.
16.2
c. Define the
related automata
A
and
C
and carry on the following automata computations:
1.
C
2.
C
\ .IO/
?
3.
.C \
.I
O/
?
/
*U[V
4.
A \ .
C
\ .IO/
?
/
*U[V
5.
.A \ .
C
\ .IO/
?
/
*U[V
/
+U[V
6.
.A \ .C
\ .IO/
?
/
*U[V
/
+U[V
7.
.A \ .C
\ .IO/
?
/
*U[V
/
+U[V
\ .U V /
?
16.2.
Solve the FSM equation
M
A
˘ M
X
Š M
C
,where
M
A
is the context FSM
shown in Fig.
16.2
a, and
M
C
is the specification FSM in Fig.
16.2
c. Given the
solution of the companion FSM equation
M
A
˘M
X
M
C
obtained in Problem
16.1
,
how does one solve this FSM equation?
16.3.
Consider the parallel composition in Fig.
16.1
,where
M
A
is the context FSM
shown in Fig.
16.2
a, and
M
C
is the specification FSM in Fig.
16.2
c.
Given the implementations
Imp1
and
Imp2
of the FSM
Emb
, shown respectively
in Fig.
16.4
a, b, for each implementation find external test suites to detect whether
it is faulty, based on the information provided by the largest solution of the related
FSM equation.
b
a
u
1
/
v
2
u
1
/
v
2
u
1
/
v
1
u
1
/
v
1
u
2
/
v
1
u
2
/
v
2
u
2
/
v
2
u
2
/
v
1
c
u
1
/
v
2
u
2
/
v
2
Fig. 16.4
(
a
) FSM
Imp1
;(
b
) FSM
Imp2
;(
c
) FSM
Imp2
Search WWH ::
Custom Search