// Modest model of the Bounded Retransmission Protocol (BRP) action put, get, put_k, get_k, put_l, get_l; action new_file; action s_ok, s_dk, s_nok, s_restart; action r_ok, r_inc, r_fst, r_nok, r_timeout; exception error, channel_overflow, premature_timeout; // Constants const int N; // number of frames per file const int MAX; // maximum number of retransmissions per frame const int TD; // transmission delay const int TS = 2 * TD + 1; // sender timeout const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout const int SYNC = TR; bool ff, lf, ab; // Channel data: first/last frame, alternating bit int i limit [0..N]; // Sender chunk counter bool inTransitK = false; bool inTransitL = false; bool first_file_done = false; // Properties bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen; // Invariant (timed) properties (from [BrpOnTime], the TA model) // "there is at most one message in transit for each channel" property T_1 = A[] (!did(channel_overflow)); // "there is at most one message in transit in total" property T_2 = A[] (!(inTransitK && inTransitL)); // Assumption (A1): "no premature timeouts" property T_A1 = A[] (!did(premature_timeout)); // Assumption (A2): "sender starts new file only after receiver reacted to failure" // Note that receiver can only notice failure if it received at least one chunk, i.e. did(get_k) property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen); // Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model) // property A of [D'AJJL01]: "the maximum probability that eventually the sender reports // a certain unsuccessful transmission but the receiver got the complete file" property P_A = Pmax(<> s_nok_seen && r_ok_seen); // property B of [D'AJJL01]: "the maximum probability that eventually the sender reports // a certain successful transmission but the receiver did not get the complete file" property P_B = Pmax(<> s_ok_seen && !r_ok_seen); // property 1 of [D'AJJL01]: "the maximum probability that eventually the sender // does not report a successful transmission" property P_1 = Pmax(<> s_nok_seen || s_dk_seen); // property 2 of [D'AJJL01]: "the maximum probability that eventually the sender // reports an uncertainty on the success of the transmission" property P_2 = Pmax(<> s_dk_seen); // property 3 of [D'AJJL01]: "the maximum probability that eventually the sender // reports an unsuccessful transmission after more than 8 chunks have been sent successfully" property P_3 = Pmax(<> s_nok_seen && i > 8); // property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver // does not receive any chunk and the sender tried to send a chunk" property P_4 = Pmax(<> (s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen); // Probabilistic time-bounded reachability properties // "the maximum/minimum probability that the sender reports // a successful transmission within 64 time units" property Dmax = Pmax(<> s_ok_seen && time <= 64); property Dmin = Pmin(<> s_ok_seen && time <= 64); // Expected reachability properties // "the maximum/minimum expected time until the transfer // of the first file is finished (successfully or unsuccessfully)" property Emax = Xmax(time | first_file_done); property Emin = Xmin(time | first_file_done); process Sender() { exception timeout; bool bit; clock c; process LinkLayerSendData() { clock c; invariant(c <= 0) put_k {= ff=(i==1), lf=(i==N), ab=bit =} } process LinkLayerReceiveAck() { get_l } process WaitAck() { clock c; invariant(c <= TS) alt { :: LinkLayerReceiveAck(); urgent break :: when(c == TS) throw(timeout) } } process SendChunk() { int rc limit [0..MAX]; do { :: try { urgent tau par { :: LinkLayerSendData() :: WaitAck() } } catch timeout { alt { :: when(rc < MAX) urgent {= rc=rc+1 =} // retry :: when(rc == MAX) urgent throw(error) // no retries left } } } } invariant(c <= 0) new_file {= i=0 =}; try { do { :: when(i < N) urgent {= i=i+1 =}; SendChunk(); urgent {= bit=!bit =} :: when(i == N) // file transmission successfully completed urgent s_ok {= first_file_done=true =}; urgent break } } catch error { urgent alt { :: when(i < N) s_nok {= c=0 =} :: when(i == N) s_dk {= c=0 =} }; // file transmission not successful invariant(c <= SYNC) when(c == SYNC) s_restart {= c=0, bit=false, first_file_done=true =} }; Sender() } process Receiver() { exception timeout; bool r_ff, r_lf, r_ab; bool bit; clock c; process LinkLayerReceiveData() { get_k {= c=0, bit=ab, r_ff=ff, r_lf=lf, r_ab=ab =} } process LinkLayerSendAck() { invariant(c <= 0) put_l } process WaitData() { invariant(c <= TR) alt { :: LinkLayerReceiveData() :: when(c == TR) throw(timeout) } } // receive the first frame of a file LinkLayerReceiveData(); urgent alt { :: when(ff) tau :: when(!ff) throw(premature_timeout) }; // receive the rest of the file do { :: // report frame to upper layer urgent alt { :: when(r_ab != bit) tau // repetition :: when(r_ab == bit) alt { :: when(r_lf) r_ok {= bit=!bit =} :: when(!r_lf && r_ff) r_fst {= bit=!bit =} :: when(!r_lf && !r_ff) r_inc {= bit=!bit =} } }; // acknowledge LinkLayerSendAck(); // wait for next frame try { WaitData() } catch timeout { urgent r_timeout; urgent alt { :: when(r_lf) break // we just got the last frame :: when(!r_lf) r_nok; urgent break // abort transfer } } }; Receiver() } process ChannelK() { clock c; put_k palt { :98: {= c = 0, inTransitK = true =}; invariant(c <= TD) alt { :: get_k {= inTransitK = false =} :: put_k {==}; urgent throw(channel_overflow) } :2: {==} }; ChannelK() } process ChannelL() { clock c; put_l palt { :99: {= c = 0, inTransitL = true =}; invariant(c <= TD) alt { :: get_l {= inTransitL = false =} :: put_l {==}; urgent throw(channel_overflow) } :1: {==} }; ChannelL() } process Tester() // prevents more than one file being sent { new_file } process Observer() { do { :: get_k {= get_k_seen = true =} :: s_ok {= s_ok_seen = true =} :: s_nok {= s_nok_seen = true =} :: s_dk {= s_dk_seen = true =} :: s_restart {= s_restart_seen = true =} :: r_ok {= r_ok_seen = true =} :: r_timeout {= r_timeout_seen = true =} } } par { :: Sender() :: Receiver() :: ChannelK() :: ChannelL() :: Tester() :: Observer() }