www.prismmodelchecker.org

Bounded Retransmission Protocol

(D'Argenio, Jeannet, Jensen & Larsen)

Contents

Introduction

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
View: printable version          Download: brp.pm

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.

Model Statistics

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:
162 6772,1826
163 8862,1796
1641,0952,2376
1651,3042,2306
3221,3492,2726
3231,7662,2696
3242,1832,3276
3252,6002,3206
6422,6932,3626
6433,5262,3596
6444,3592,4176
6455,1922,4106

Model Construction Times

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:
1620.120.10105
1630.120.11107
1640.140.12109
1650.150.12111
3220.220.22201
3230.270.22203
3240.280.26205
3250.280.25207
6420.500.42393
6430.520.43395
6440.550.43397
6450.580.44399

Model Checking

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 ]
View: printable version          Download: brp.pctl

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):
    1620.001
    1630.001
    1640.001
    1650.001
    3220.002
    3230.002
    3240.002
    3250.002
    6420.002
    6430.002
    6440.001
    6450.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):
    1620.001
    1630.002
    1640.002
    1650.001
    3220.002
    3230.002
    3240.002
    3250.002
    6420.002
    6430.002
    6440.002
    6450.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:
    1620.01110.11970.011254.23E-4
    1630.01130.10970.011271.26E-5
    1640.01150.11970.011313.76E-7
    1650.01170.10970.011331.12E-8
    3220.01110.181930.022258.46E-4
    3230.01130.181930.022292.52E-5
    3240.01150.211930.022317.52E-7
    3250.01170.221930.022352.24E-8
    6420.01110.383850.034250.001692
    6430.01130.373850.044275.05E-5
    6440.01150.423850.054311.51E-6
    6450.01170.443850.064334.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:
    1620.101000.019 0.011272.64E-5
    1630.101020.01110.011317.89E-7
    1640.081040.01130.011352.35E-8
    1650.081060.01150.011377.00E-10
    3220.152960.019 0.012292.64E-5
    3230.151980.02110.012337.89E-7
    3240.172000.01130.022372.35E-8
    3250.192020.02150.022397.00E-10
    6420.323880.019 0.034312.64E-5
    6430.353900.01110.044357.89E-7
    6440.373920.01130.054372.35E-8
    6450.373940.01150.064417.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:

    58606264
    N: MAX:   Precomputation:   Main Algorithm:   Probability:
    Prob1E Prob0A Time (s): Iterations:
    Time (s): Iterations: Time (s): Iterations:
    1620.05580.07430.011191.85E-4
    1630.05600.07430.011235.52E-6
    1640.05620.07430.011251.65E-7
    1650.05640.07430.011294.90E-9
    3220.05580.161390.012196.08E-4
    3230.06600.151390.012231.81E-5
    3240.05620.181390.022255.41E-7
    3250.05640.201390.022291.61E-8
    6420.070.383310.034190.001454
    6430.050.423310.044214.34E-5
    6440.060.423310.054251.29E-6
    6450.060.433310.064273.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:
    1620.019 0.0130.0178.00E-6
    1630.01110.0130.019 1.60E-7
    1640.01130.0130.01113.20E-9
    1650.01150.0130.01136.40E-11
    3220.019 0.0130.0178.00E-6
    3230.01110.0130.019 1.60E-7
    3240.01130.0130.01113.20E-9
    3250.01150.0130.01136.40E-11
    6420.019 0.0130.017 8.00E-6
    6430.01110.0130.019 1.60E-7
    6440.01130.0130.01113.20E-9
    6450.01150.0130.01136.40E-11

Case Studies