// 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() { bool bit; int rc limit [0..MAX]; clock c; do { :: invariant(c <= 0) new_file {= i=0, rc=0 =}; try { do { :: when(i < N) urgent {= i=i+1 =}; do { :: // send frame invariant(c <= 0) put_k {= ff=(i==1), lf=(i==N), ab=bit, c=0 =}; invariant(c <= TS) alt { :: get_l {= bit=!bit, rc=0, c=0 =}; // ack received urgent break :: when(c == TS && rc < MAX) // timeout, retry {= rc=rc+1, c=0 =} :: when(c == TS && rc == MAX && i < N) // timeout, no retries left s_nok {= rc=0, c=0 =}; urgent throw(error) :: when(c == TS && rc == MAX && i == N) // timeout, no retries left s_dk {= rc=0, c=0 =}; urgent throw(error) } } :: when(i == N) // file transmission successfully completed urgent s_ok {= first_file_done=true =}; urgent break } } catch error { // File transfer did not succeed: wait, then restart with next file invariant(c <= SYNC) when(c == SYNC) s_restart {= bit=false, first_file_done=true =} } } } process Receiver() { bool r_ff, r_lf, r_ab; bool bit; clock c; // receive first frame alt { :: when(ff) get_k {= c=0, bit=ab, r_ff=ff, r_lf=lf, r_ab=ab =} :: when(!ff) get_k {= c=0 =}; urgent throw(premature_timeout) }; do { :: invariant(c <= 0) alt { :: when(r_ab != bit) put_l // repetition, re-ack :: when(r_ab == bit) alt { // report frame :: when(r_lf) r_ok :: when(!r_lf && r_ff) r_fst :: when(!r_lf && !r_ff) r_inc }; invariant(c <= 0) put_l {= bit=!bit =} }; invariant(c <= TR) alt { :: // receive next frame get_k {= c=0, r_ff=ff, r_lf=lf, r_ab=ab =} :: // timeout when(c == TR) alt { :: when(r_lf) // we just got the last frame, though r_timeout; urgent break :: when(!r_lf) r_nok; // abort transfer urgent r_timeout; urgent break } } }; Receiver() } process ChannelK() { clock c; do { :: put_k palt { :98: {= c = 0, inTransitK = true =}; invariant(c <= TD) alt { :: get_k {= inTransitK = false =} :: put_k {==}; urgent throw(channel_overflow) } :2: {==} } } } process ChannelL() { clock c; do { :: put_l palt { :99: {= c = 0, inTransitL = true =}; invariant(c <= TD) alt { :: get_l {= inTransitL = false =} :: put_l {==}; urgent throw(channel_overflow) } :1: {==} } } } 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() }