Download CHAPTER I A CONCEPTUAL FRAMEWORK FOR TESTING

UserInt?ClearReq:ClearReq_type;
NetInt!Disc; DTE[UserInt,NetInt] (s0 )
[]
UserInt?Digit:Digit_type;
NetInt!Info; DTE[UserInt,NetInt] (s3 )
[]
NetInt?Prog:Prog_type;
UserInt!Announce; DTE[UserInt,NetInt] (s6 )
[]
NetInt?Alert:Alert_type;
UserInt!RingBack; DTE[UserInt,NetInt] (s4 )
)
[]
[s = s4 ] ->
(
UserInt?ClearReq:ClearReq_type;
NetInt!Disc; DTE[UserInt,NetInt] (s0 )
[]
NetInt?Disc:Disc_type;
UserInt!StopRingBack; DTE[UserInt,NetInt] (s6 )
[]
NetInt?Con:Con_type;
UserInt!ConAck; DTE[UserInt,NetInt] (s5 )
)
[]
[s = s5 ] ->
(
UserInt?ClearReq:ClearReq_type;
NetInt!Disc; DTE[UserInt,NetInt] (s0 )
[]
NetInt?Disc:Disc_type;
UserInt!StopCon; DTE[UserInt,NetInt] (s6 )
)
[]
[s = s6 ] ->
UserInt?ClearReq:ClearReq_type;
DTE[UserInt,NetInt] (s0 )
endproc (*end of process DTE*)
endproc (*end of behavior*)
endspec
I.21