1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
/*
* Session Layer Validation Model
*/
proctype session(bit n)
{ bit toggle;
byte type, status;
endIDLE:
do
:: pres_to_ses[n]?type ->
if
:: (type == transfer) ->
goto DATA_OUT
:: (type != transfer) /* ignore */
fi
:: flow_to_ses[n]?type,0 ->
if
:: (type == connect) ->
goto DATA_IN
:: (type != connect) /* ignore */
fi
od;
DATA_IN: /* 1. prepare local file fsrver */
ses_to_fsrv[n]!create;
do
:: fsrv_to_ses[n]?reject ->
ses_to_flow[n]!reject,0;
goto endIDLE
:: fsrv_to_ses[n]?accept ->
ses_to_flow[n]!accept,0;
break
od;
/* 2. Receive the data, upto eof */
do
:: flow_to_ses[n]?data,0 ->
ses_to_fsrv[n]!data
:: flow_to_ses[n]?eof,0 ->
ses_to_fsrv[n]!eof;
break
:: pres_to_ses[n]?transfer ->
ses_to_pres[n]!reject(NON_FATAL)
:: flow_to_ses[n]?close,0 -> /* remote user aborted */
ses_to_fsrv[n]!close;
break
:: timeout -> /* got disconnected */
ses_to_fsrv[n]!close;
goto endIDLE
od;
/* 3. Close the connection */
ses_to_flow[n]!close,0;
goto endIDLE;
DATA_OUT: /* 1. prepare local file fsrver */
ses_to_fsrv[n]!open;
if
:: fsrv_to_ses[n]?reject ->
ses_to_pres[n]!reject(FATAL);
goto endIDLE
:: fsrv_to_ses[n]?accept ->
skip
fi;
/* 2. initialize flow control */
ses_to_flow[n]!sync,toggle;
do
:: atomic {
flow_to_ses[n]?sync_ack,type ->
if
:: (type != toggle)
:: (type == toggle) -> break
fi
}
:: timeout ->
ses_to_fsrv[n]!close;
ses_to_pres[n]!reject(FATAL);
goto endIDLE
od;
toggle = 1 - toggle;
/* 3. prepare remote file fsrver */
ses_to_flow[n]!connect,0;
if
:: flow_to_ses[n]?reject,0 ->
ses_to_fsrv[n]!close;
ses_to_pres[n]!reject(FATAL);
goto endIDLE
:: flow_to_ses[n]?connect,0 ->
ses_to_fsrv[n]!close;
ses_to_pres[n]!reject(NON_FATAL);
goto endIDLE
:: flow_to_ses[n]?accept,0 ->
skip
:: timeout ->
ses_to_fsrv[n]!close;
ses_to_pres[n]!reject(FATAL);
goto endIDLE
fi;
/* 4. Transmit the data, upto eof */
do
:: fsrv_to_ses[n]?data ->
ses_to_flow[n]!data,0
:: fsrv_to_ses[n]?eof ->
ses_to_flow[n]!eof,0;
status = COMPLETE;
break
:: pres_to_ses[n]?abort -> /* local user aborted */
ses_to_fsrv[n]!close;
ses_to_flow[n]!close,0;
status = FATAL;
break
od;
/* 5. Close the connection */
do
:: pres_to_ses[n]?abort /* ignore */
:: flow_to_ses[n]?close,0 ->
if
:: (status == COMPLETE) ->
ses_to_pres[n]!accept,0
:: (status != COMPLETE) ->
ses_to_pres[n]!reject(status)
fi;
break
:: timeout ->
ses_to_pres[n]!reject(FATAL);
break
od;
goto endIDLE
}
|
