Hardware Reference
In-Depth Information
Fig. 16.3 Solution Imp live of
the equation
Context
u 1 / v 2
q 0
q 1
˘ X Š
Spec
u 1 / v 1
u 2 / v 2
u 2 / v 1
since the submachine of the latter restricted to the states p 1 ;p 2 ;p 3 ;p 4 ;dc ( p 2 with
the transition u 2 = v 1 but no transition u 2 = v 2 ) is an “unfolding” of Emb ,where p 1 ;p 3
and dc simulate q 0 ,and p 2 and p 4 simulate q 1 .
Notice that if we choose Imp live , the solution contained in Largest shown in
Fig. 16.3 ( p 1 and dc simulate q 0 ,and p 2 and p 5 simulate q 1 ), we get a situation
where Context ˘ Imp live © Spec , due to the livelock occurring e.g., with the sequence
t 0
u 2 = v 2
! q 1 etc.
The largest solution is a complete observable FSM and following the approach
of [108] we derive from it a complete internal test suite w.r.t. the fault domain J Emb
than contains each FSM over input alphabet U with up to 2 states:
i 1 = u 1
!
u 1 = v 2
!
v 2 = u 2
!
u 2 = v 2
!
v 2 = u 2
!
t 0 , q 0
q 1 , t 0
t 0 , q 1
q 1 , t 0
t 0 , q 1
TS int
Df u 1 u 1 u 1 u 1 ; u 1 u 1 u 2 u 1 ; u 1 u 2 u 1 u 1 ; u 1 u 2 u 2 u 1 g:
The completeness of a test suite implies that for each FSM which is not a
reduction of the specification FSM a state of the product of the two machines where
they disagree on outputs for some input is traversed when some test from the test
suite followed by that input is executed. Therefore, according to Proposition 16.2 ,
the test suite TS int can be translated into a complete external test suite. Formally,
for each prefix ˛ u of each input sequence of an internal test suite TS int and each
output sequence ˇ v of the same length such that ˇ is in the set of output responses
of the largest solution to ˛ while ˇ v is not in the set of output responses of the
largest solution to ˛ u , we must determine a set TS ext u v / of external input
sequences such that, for each implementation Imp of the embedded FSM Emb
accepting the internal I/O sequence ˛ u v , there exists an external input sequence
2 TS ext u v / for which the output responses of the composition Context ˘ Imp
and of Spec to the input sequence are different.
Example 16.4 (continues from Example 16.3 ). For each prefix ˛ u of each test case
of the internal test suite TS int we derive a set of sequences ˛ u v such that ˛=ˇ is
accepted by the largest complete solution Largest of the equation Context ˘ X Š
Spec , while the I/O sequence ˛ u v is not accepted by the FSM Largest and obtain
the following subset of prefixes of TS int together with the corresponding outputs:
f u 1 = v 1 ; u 1 u 1 = v 2 v 2 ; u 1 u 1 u 1 = v 2 v 1 v 1 ; u 1 u 1 u 1 u 1 = v 2 v 1 v 2 v 2 ; u 1 u 1 u 2 = v 2 v 1 v 2 ; u 1 u 1 u 2 u 1 =
v 2 v 1 v 1 v 1 ; u 1 u 2 u 1 = v 2 v 1 v 2 ; u 1 u 2 u 1 u 1 = v 2 v 1 v 1 v 1 ; u 1 u 2 u 2 u 1 = v 2 v 2 v 1 v 2 g:
Notice that u 1 u 2 and u 1 u 2 u 2 are not in the set because they do not satisfy the
conditions that ˛=ˇ is in Largest , while ˛ u v is not.
 
Search WWH ::




Custom Search