(D'Argenio, Jeannet, Jensen & Larsen)

This case study is based on the bounded retransmission protocol (BRP) [HSV94], a variant of
the alternating bit protocol. The BRP protocol sends a file in a number of chunks,
but allows only a bounded number of retransmissions of each chunk.
The model is represented as an MDP.
We let **N** denote the number of chunks and **MAX** the maximum allowed number of retransmissions of each chunk.
The PRISM source code is given below.

// bounded retransmission protocol [D'AJJL01] // gxn/dxp 23/05/2001 dtmc // number of chunks const int N; // maximum number of retransmissions const int MAX; module sender s : [0..6]; // 0 idle // 1 next_frame // 2 wait_ack // 3 retransmit // 4 success // 5 error // 6 wait sync srep : [0..3]; // 0 bottom // 1 not ok (nok) // 2 do not know (dk) // 3 ok (ok) nrtr : [0..MAX]; i : [0..N]; bs : bool; s_ab : bool; fs : bool; ls : bool; // idle [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); // next_frame [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); // wait_ack [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); [TO_Msg] (s=2) -> (s'=3); [TO_Ack] (s=2) -> (s'=3); // retransmit [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); // success [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); [] (s=4) & (i=N) -> (s'=0) & (srep'=3); // error [SyncWait] (s=5) -> (s'=6); // wait sync [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); endmodule module receiver r : [0..5]; // 0 new_file // 1 fst_safe // 2 frame_received // 3 frame_reported // 4 idle // 5 resync rrep : [0..4]; // 0 bottom // 1 fst // 2 inc // 3 ok // 4 nok fr : bool; lr : bool; br : bool; r_ab : bool; recv : bool; // new_file [SyncWait] (r=0) -> (r'=0); [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); // fst_safe_frame [] (r=1) -> (r'=2) & (r_ab'=br); // frame_received [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); [aA] (r=2) & !(r_ab=br) -> (r'=4); // frame_reported [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); // idle [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); [SyncWait] (r=4) & (ls=true) -> (r'=5); [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); // resync [SyncWait] (r=5) -> (r'=0) & (rrep'=0); endmodule // prevents more than one file being sent module tester T : bool; [NewFile] (T=false) -> (T'=true); endmodule module channelK k : [0..2]; // idle [aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2); // sending [aG] (k=1) -> (k'=0); // lost [TO_Msg] (k=2) -> (k'=0); endmodule module channelL l : [0..2]; // idle [aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2); // sending [aB] (l=1) -> (l'=0); // lost [TO_Ack] (l=2) -> (l'=0); endmodule

We note that, as in [DJJL01], we have added a checker process which ensures that when checking properties we are only considering the transmission of one file, that is, we are not interested in checking properties after a transmission was successful or unsuccessful.

The table below shows statistics for each model we have built.
The first section gives the number of **states** in the MDP representing the model.
The second part refers to the MTBDD which represents this MDP:
the total number of **nodes** and
the number of **leaves** (terminal nodes).

N: |
MAX: |
Model: |
MTBDD: |
|||

States: |
Nodes: |
Leaves: |
||||

16 | 2 | 677 | 2,182 | 6 | ||

16 | 3 | 886 | 2,179 | 6 | ||

16 | 4 | 1,095 | 2,237 | 6 | ||

16 | 5 | 1,304 | 2,230 | 6 | ||

32 | 2 | 1,349 | 2,272 | 6 | ||

32 | 3 | 1,766 | 2,269 | 6 | ||

32 | 4 | 2,183 | 2,327 | 6 | ||

32 | 5 | 2,600 | 2,320 | 6 | ||

64 | 2 | 2,693 | 2,362 | 6 | ||

64 | 3 | 3,526 | 2,359 | 6 | ||

64 | 4 | 4,359 | 2,417 | 6 | ||

64 | 5 | 5,192 | 2,410 | 6 |

The table below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. We give the overall construction time and both the time and iterations for the reachability process.

N: |
MAX: |
Construction: |
Reachability: |
|||

Time (s): |
Time (s): |
Iter.s: |
||||

16 | 2 | 0.12 | 0.10 | 105 | ||

16 | 3 | 0.12 | 0.11 | 107 | ||

16 | 4 | 0.14 | 0.12 | 109 | ||

16 | 5 | 0.15 | 0.12 | 111 | ||

32 | 2 | 0.22 | 0.22 | 201 | ||

32 | 3 | 0.27 | 0.22 | 203 | ||

32 | 4 | 0.28 | 0.26 | 205 | ||

32 | 5 | 0.28 | 0.25 | 207 | ||

64 | 2 | 0.50 | 0.42 | 393 | ||

64 | 3 | 0.52 | 0.43 | 395 | ||

64 | 4 | 0.55 | 0.43 | 397 | ||

64 | 5 | 0.58 | 0.44 | 399 |

The PRISM source code for the properties considered is given below.

// property A of [D'AJJL01] // the probability the sender reports a certain unsuccessful transmission but the receiver got the complete file P=?[ F srep=1 & rrep=3 & recv ] // property B of [D'AJJL01] // the probability the sender reports a certain successful transmission but the receiver did not get the complete file P=?[ F srep=3 & !(rrep=3) & recv ] // property 1 of [D'AJJL01] // the probability the sender does not report a successful transmission P=?[ F s=5 ] // property 2 of [D'AJJL01] // the probability the sender reports an uncertainty on the success of the transmission P=?[ F s=5 & srep=2 ] // property 3 of [D'AJJL01] // the probability the sender reports an unsuccessful transmission after more than 8 chunks have been sent successfully P=?[ F s=5 & srep=1 & i>8 ] // property 4 of [D'AJJL01] // the probability the receiver does not receive any chunk and the sender tried to send a chunk P=?[ F !(srep=0) & !recv ]

There are two precomputation steps in the model checking procedure involving
BDD based fixpoint algorithms: **Prob0** and **Prob1**
which finds those states such that the probability
of satisfying the formula is 0 and 1 respectively.

In the main algorithm we use the Jacobi iterative method and stop iterating when the *relative
error* between subsequent iteration vectors is less than 1e-6,
that is:

**Property A of [DJJL01]:**"The probability the sender reports a certain unsuccessful transmission but the receiver got the complete file."**Model checking times:**As in none of the reachable states the sender reports a certain unsuccessful transmission while the receiver got the complete file, the probability of satisfying this property is 0 and model checking reduces to an invariance check.**N:****MAX:****Time (s):**16 2 0.001 16 3 0.001 16 4 0.001 16 5 0.001 32 2 0.002 32 3 0.002 32 4 0.002 32 5 0.002 64 2 0.002 64 3 0.002 64 4 0.001 64 5 0.002 **Property B of [DJJL01]:**"The probability the sender reports a certain successful transmission but the receiver did not get the complete file."**Model checking times:**As in none of the reachable states the sender reports a certain unsuccessful transmission while the receiver got the complete file, the probability of satisfying this property is 0 and model checking reduces to an invariance check.**N:****MAX:****Time (s):**16 2 0.001 16 3 0.002 16 4 0.002 16 5 0.001 32 2 0.002 32 3 0.002 32 4 0.002 32 5 0.002 64 2 0.002 64 3 0.002 64 4 0.002 64 5 0.002 **Property 1 of [DJJL01]:**"The probability the sender does not report a successful transmission."**Model checking times:****N:****MAX:****Precomputation:****Main Algorithm:****Probability:****Prob0****Prob1****Time (s):****Iterations:****Time (s):****Iterations:****Time (s):****Iterations:**16 2 0.01 11 0.11 97 0.01 125 4.23E-4 16 3 0.01 13 0.10 97 0.01 127 1.26E-5 16 4 0.01 15 0.11 97 0.01 131 3.76E-7 16 5 0.01 17 0.10 97 0.01 133 1.12E-8 32 2 0.01 11 0.18 193 0.02 225 8.46E-4 32 3 0.01 13 0.18 193 0.02 229 2.52E-5 32 4 0.01 15 0.21 193 0.02 231 7.52E-7 32 5 0.01 17 0.22 193 0.02 235 2.24E-8 64 2 0.01 11 0.38 385 0.03 425 0.001692 64 3 0.01 13 0.37 385 0.04 427 5.05E-5 64 4 0.01 15 0.42 385 0.05 431 1.51E-6 64 5 0.01 17 0.44 385 0.06 433 4.48E-8 **Property 2 of [DJJL01]:**"The probability the sender reports an uncertainty on the success of the transmission."**Model checking times:****N:****MAX:****Precomputation:****Main Algorithm:****Probability:****Prob0****Prob1****Time (s):****Iterations:****Time (s):****Iterations:****Time (s):****Iterations:**16 2 0.10 100 0.01 9 0.01 127 2.64E-5 16 3 0.10 102 0.01 11 0.01 131 7.89E-7 16 4 0.08 104 0.01 13 0.01 135 2.35E-8 16 5 0.08 106 0.01 15 0.01 137 7.00E-10 32 2 0.15 296 0.01 9 0.01 229 2.64E-5 32 3 0.15 198 0.02 11 0.01 233 7.89E-7 32 4 0.17 200 0.01 13 0.02 237 2.35E-8 32 5 0.19 202 0.02 15 0.02 239 7.00E-10 64 2 0.32 388 0.01 9 0.03 431 2.64E-5 64 3 0.35 390 0.01 11 0.04 435 7.89E-7 64 4 0.37 392 0.01 13 0.05 437 2.35E-8 64 5 0.37 394 0.01 15 0.06 441 7.00E-10 **Property 3 of [DJJL01]:**"The probability the sender reports an unsuccessful transmission after more than 8 chunks have been sent successfully."**Model checking times:****N:****MAX:****Precomputation:****Main Algorithm:****Probability:****Prob1E****Prob0A****Time (s):****Iterations:****Time (s):****Iterations:****Time (s):****Iterations:**16 2 0.05 58 0.07 43 0.01 119 1.85E-4 16 3 0.05 60 0.07 43 0.01 123 5.52E-6 16 4 0.05 62 0.07 43 0.01 125 1.65E-7 16 5 0.05 64 0.07 43 0.01 129 4.90E-9 32 2 0.05 58 0.16 139 0.01 219 6.08E-4 32 3 0.06 60 0.15 139 0.01 223 1.81E-5 32 4 0.05 62 0.18 139 0.02 225 5.41E-7 32 5 0.05 64 0.20 139 0.02 229 1.61E-8 64 2 0.07 0.38 331 0.03 419 0.001454 64 3 0.05 0.42 331 0.04 421 4.34E-5 64 4 0.06 0.42 331 0.05 425 1.29E-6 64 5 0.06 0.43 331 0.06 427 3.85E-8 **Property 4 of [DJJL01]:**"The probability the receiver does not receive any chunk and the sender tried to send a chunk."**Model checking times:****N:****MAX:****Precomputation:****Main Algorithm:****Probability:****Prob1E****Prob0A****Time (s):****Iterations:****Time (s):****Iterations:****Time (s):****Iterations:**16 2 0.01 9 0.01 3 0.01 7 8.00E-6 16 3 0.01 11 0.01 3 0.01 9 1.60E-7 16 4 0.01 13 0.01 3 0.01 11 3.20E-9 16 5 0.01 15 0.01 3 0.01 13 6.40E-11 32 2 0.01 9 0.01 3 0.01 7 8.00E-6 32 3 0.01 11 0.01 3 0.01 9 1.60E-7 32 4 0.01 13 0.01 3 0.01 11 3.20E-9 32 5 0.01 15 0.01 3 0.01 13 6.40E-11 64 2 0.01 9 0.01 3 0.01 7 8.00E-6 64 3 0.01 11 0.01 3 0.01 9 1.60E-7 64 4 0.01 13 0.01 3 0.01 11 3.20E-9 64 5 0.01 15 0.01 3 0.01 13 6.40E-11