1/* 2 * PROMELA Validation Model 3 * FLOW CONTROL LAYER VALIDATION 4 */ 5 6/* see end of file for LTL properties */ 7 8#define LOSS 1 /* message loss */ 9#define DUPS 0 /* duplicate msgs */ 10#define QSZ 2 /* queue size */ 11 12mtype = { 13 red, white, blue, 14 abort, accept, ack, sync_ack, close, connect, 15 create, data, eof, open, reject, sync, transfer, 16 FATAL, NON_FATAL, COMPLETE 17 } 18 19chan ses_to_flow[2] = [QSZ] of { byte, byte }; 20chan flow_to_ses[2] = [QSZ] of { byte, byte }; 21chan dll_to_flow[2] = [QSZ] of { byte, byte }; 22 23/* 24 * Flow Control Layer Validation Model 25 */ 26 27#define true 1 28#define false 0 29 30#define M 4 /* range sequence numbers */ 31#define W 2 /* window size: M/2 */ 32 33proctype fc(chan s2f, f2d, f2s, d2f) 34{ bool busy[M]; /* outstanding messages */ 35 byte q; /* seq# oldest unacked msg */ 36 byte m; /* seq# last msg received */ 37 byte s; /* seq# next msg to send */ 38 byte window; /* nr of outstanding msgs */ 39 byte type; /* msg type */ 40 bit received[M]; /* receiver housekeeping */ 41 bit x; /* scratch variable */ 42 byte p; /* seq# of last msg acked */ 43 byte I_buf[M], O_buf[M]; /* message buffers */ 44 45 xr s2f; 46 xs f2d; 47 xs f2s; 48 xr d2f; 49 50 /* sender part */ 51end: do 52 :: atomic { 53 (window < W && nempty(s2f) 54 && nfull(f2d)) -> 55 s2f?type,x; 56 window = window + 1; 57 busy[s] = true; 58 O_buf[s] = type; 59 f2d!type,s; 60 if 61 :: (type != sync) -> 62 s = (s+1)%M 63 :: (type == sync) -> 64 window = 0; 65 s = M; 66 do 67 :: (s > 0) -> 68 s = s-1; 69 busy[s] = false 70 :: (s == 0) -> 71 break 72 od 73 fi 74 } 75 :: atomic { 76 (window > 0 && busy[q] == false) -> 77 window = window - 1; 78 q = (q+1)%M 79 } 80#if DUPS 81 :: atomic { 82 (nfull(f2d) && window > 0 && busy[q] == true) -> 83 f2d!O_buf[q],q 84 } 85#endif 86 :: atomic { 87 (timeout && nfull(f2d) && window > 0 && busy[q] == true) -> 88 f2d!O_buf[q],q 89 } 90 /* receiver part */ 91#if LOSS 92 :: d2f?type,m /* lose any message */ 93#endif 94 :: d2f?type,m -> 95 if 96 :: atomic { 97 (type == ack) -> 98 busy[m] = false 99 } 100 :: atomic { 101 (type == sync) -> 102 m = 0; 103 do 104 :: (m < M) -> 105 received[m] = 0; 106 m = m+1 107 :: (m == M) -> 108 break 109 od 110 }; f2d!sync_ack,0 111 :: (type == sync_ack) -> 112 f2s!sync_ack,0 113 :: (type != ack && type != sync && type != sync_ack)-> 114 if 115 :: atomic { 116 (received[m] == true) -> 117 x = ((0<p-m && p-m<=W) 118 || (0<p-m+M && p-m+M<=W)) }; 119 if 120 :: (x) -> f2d!ack,m 121 :: (!x) /* else skip */ 122 fi 123 :: atomic { 124 (received[m] == false) -> 125 I_buf[m] = type; 126 received[m] = true; 127 received[(m-W+M)%M] = false 128 } 129 fi 130 fi 131 :: /* atomic { */ 132 (received[p] == true && nfull(f2s) && nfull(f2d)) -> 133 f2s!I_buf[p],0; 134 f2d!ack,p; 135 p = (p+1)%M 136 /* } */ 137 od 138} 139 140proctype upper_s(chan s2f, f2s0) 141{ byte s_state; 142 byte type, toggle; 143 144 xs s2f; 145 xr f2s0; 146 147 s2f!sync,toggle; 148 do 149 :: f2s0?sync_ack,type -> 150 if 151 :: (type != toggle) 152 :: (type == toggle) -> break 153 fi 154 :: timeout -> 155 s2f!sync,toggle 156 od; 157 toggle = 1 - toggle; 158 159end: do 160 :: s2f!white,0 161 :: atomic { 162 (s_state == 0 && nfull(s2f)) -> 163 s2f!red,0 -> 164 s_state = 1 165 } 166 :: atomic { 167 (s_state == 1 && nfull(s2f)) -> 168 s2f!blue,0 -> 169 s_state = 2 170 } 171 od 172} 173 174proctype upper_r(chan f2s1) 175{ byte r_state; 176 177 xr f2s1; 178 179 do 180 :: f2s1?white,0 181 :: f2s1?red,0 -> break 182 :: f2s1?blue,0 -> assert(0) 183 od; 184 185 do 186 :: f2s1?white,0 187 :: f2s1?red,0 -> assert(0) 188 :: f2s1?blue,0 -> goto end 189 od; 190end: 191 do 192 :: f2s1?white,0 193 :: f2s1?red,0 -> assert(0) 194 :: f2s1?blue,0 -> assert(0) 195 od 196} 197 198init 199{ 200 atomic { 201 run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]); 202 run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]); 203 run upper_s(ses_to_flow[0], flow_to_ses[0]); 204 run upper_r(flow_to_ses[1]) 205 } 206} 207 208ltl p1 { ( len(flow_to_ses[1]) > 0 -> flow_to_ses[1]?[white]) U ( flow_to_ses[1]?[red] ) } 209ltl p2 { (!(flow_to_ses[1]?[blue])) U (flow_to_ses[1]?[red]) } 210ltl p3 { <> (flow_to_ses[1]?[blue]) } 211