#include "dtime.h" /*BRP parameters according to D'Argenio et al. "The Bounded Retransmission Protocol Must Be on Time!", TACAS'97, 1997 Almost all denotations are the same as in their article*/ #define TD 1 /* transmission delay */ #define T1 3 /* sender's timout*/ #define MAX 3 /*nr of maximal retransmissions */ #define n 3 /*nr of chunks*/ #define TR 21 /* 2*MAX*T1+3*TD* receiver's timeout*/ #define SYNC 21 /*can be taken =TR*/ /*********/ /* Lists - written by Dennis Dams */ /*********/ /* A list is represented by an array (field lst) of maximal length N. The field nonempty can be seen as a pointer to the first free cell of the array. The last non-free cell (highest index) in the array represents the head of the list. */ typedef List{ byte nonempty; /* Length of list. */ byte lst[n]; /* The list. */ byte i; /* Auxiliary. */ }; #define HasOneElem(l) (l.nonempty == 1) #define Head(l) (l.lst[l.nonempty - 1]) #define RemHead(l) l.nonempty = l.nonempty - 1 /* Append(e,l) appends element e to the end of list l (and hence in front of the array lst) . */ #define Append(e,l) \ l.i = l.nonempty; \ do \ :: l.i > 0 -> \ l.lst[l.i] = l.lst[l.i - 1]; \ l.i = l.i - 1 \ :: else -> break \ od; l.lst[l.i] = e; \ l.nonempty = l.nonempty + 1 /* MakeListEmpty(l) makes l (really) empty by setting everything to 0 (cf. ReadInd). */ #define MakeListEmpty(l) \ do \ :: l.nonempty > 0 -> \ l.nonempty = l.nonempty - 1; \ l.lst[l.nonempty] = 0 \ :: else -> break \ od;l.i = 0 /* CheckAndMakeEmpty(l) also makes list l empty. */ #define CheckAndMakeEmpty(l) MakeListEmpty(l) /* CreateList(l,N,s) creates in l a list of length N, filled with successive numbers starting at s. (Recall that the head of the list is the last element in the array.) */ #define CreateList(l,N,s) \ l.i = 0; \ do \ :: l.i < N -> l.lst[(N - 1) - l.i] = s + l.i; l.i = l.i + 1 \ :: else -> break \ od; \ l.nonempty = l.i; \ l.i = 0 List list, reclist; /*message types*/ #define I_OK 100 #define I_DK 101 #define I_NOK 102 #define I_FST 103 #define I_INC 104 #define ack 1 #define START 0 #define COMM_STAT 1 /*all (Promela) channels are of rendez-vous type*/ chan F = [0] of {bit, bit, bit, byte}; chan G = [0] of {bit, bit, bit, byte}; chan A = [0] of {bit}; chan B = [0] of {bit}; chan Sin = [0] of {List}; chan Sout = [0] of {byte}; chan Rout = [0] of {byte, byte} chan SCtoF = [0] of {bit}; /*Sending client to File*/ chan RCtoF = [0] of {bit}; /*Receiving client to File*/ /*The model mimics the one written in UPPAAL in D'Argenio et al. Sender and Receiver processes correspond to sender S and receiver R as presented in Section 5 (Figures 1 and 2). Channels are modeled following the considerations in 6.1. The sender and receiver client processes, SClient and RClient as well as File process are analogous to the processes with the same names from 6.2 (Figure 6).*/ proctype SClient(chan toFile) { ok: toFile!START; goto send_req; dk: toFile!START; goto send_req; nok: toFile!START; goto send_req; send_req: CreateList(list,n,1); Sin!list; file_req: if :: Sout?I_OK -> goto ok; :: Sout?I_DK -> goto dk; :: Sout?I_NOK -> goto nok; fi; } proctype RClient(chan toFile) { byte pkt; ok: if :: Rout?I_OK,pkt -> Append(pkt,reclist) -> goto unique_rec; :: Rout?I_FST,pkt -> Append(pkt,reclist) -> goto start_rec; fi; unique_rec: toFile!COMM_STAT; CheckAndMakeEmpty(reclist); goto ok; start_rec: toFile!COMM_STAT; goto inc; inc: if :: Rout?I_OK,pkt -> Append(pkt,reclist); CheckAndMakeEmpty(reclist)-> goto ok; :: Rout?I_INC,pkt -> Append(pkt,reclist) -> goto inc; :: Rout?I_NOK,pkt -> CheckAndMakeEmpty(reclist)-> goto nok; fi; nok: if :: Rout?I_FST,pkt -> Append(pkt,reclist) -> goto start_rec; :: Rout?I_OK,pkt -> /* Never enabled when lists > 1. */ Append(pkt,reclist) -> goto unique_rec; fi; } proctype File(chan fromSC, fromRC) { same: if :: fromRC?COMM_STAT -> goto same; :: fromSC?START -> goto other; fi; other: if :: fromRC?COMM_STAT -> goto same; :: fromSC?START -> goto other; fi; } proctype Sender(chan in, out) { timer x; byte i /*, di*/; /*chunk seq. number, chunk*/ bit ab=0; /* sequence number*/ byte rc=0; /*nr of retransmitions*/ idle: Sin?list; atomic{printf("MSC: New\n");/*di=0*/; i=1;}; next_frame: /*atomic{ di = (di+1)%n;*/ rc = 0; /*}*/ send_frame: set(x,T1); out!(i==1 -> 1 : 0),(i==n -> 1 : 0), ab, Head(list); wait_ack: do :: in?_ -> atomic{/* reset(x); */ ab=1-ab; goto success}; :: atomic{expire(x) -> if :: rc /* reset(x); */ rc=rc+1; goto send_frame; :: rc==MAX -> if :: i==n -> Sout!I_DK; printf("MSC: DK\n"); :: i Sout!I_NOK; printf("MSC: NOK\n"); fi; /* reset(x); */ goto error; fi;} od; success: if :: atomic{i i=i+1; goto next_frame}; :: atomic{i==n-> Sout!I_OK; goto idle;} fi; error: atomic{delay(x,SYNC); ab=0; goto idle;} } proctype Receiver(chan in, out) { timer z; byte d; /*received chunk*/ bit rb1, rbN, rab, exp_ab; /*received and expected bits*/ new_file: in?rb1,rbN,rab,d -> atomic{set(z,TR); goto first_safe_frame;} first_safe_frame: exp_ab=rab; frame_received: if :: atomic{rab==exp_ab -> if :: rbN==1 -> Rout!I_OK,d; printf("MSC: OK\n"); :: rbN==0 && rb1==0 -> Rout!I_INC,d; printf("MSC: INC\n"); :: rbN==0 && rb1==1 -> Rout!I_FST,d; printf("MSC: FST\n"); fi; goto frame_reported;} :: atomic{rab!=exp_ab -> goto idle;} fi; frame_reported: atomic{out!ack; exp_ab=1-exp_ab; set(z,TR); goto idle}; idle: do /* z <= TR */ :: in?rb1, rbN, rab, d; goto frame_received; :: atomic{expire(z) -> if :: rbN==1 -> /* reset(z); */ goto new_file; :: rbN==0 -> /* reset(z); */ Rout!I_NOK,d; printf("MSC: NOK\n"); goto new_file; fi;} od; } proctype K(chan in, out) { timer xk; byte d; /*received chunk*/ bit rb1, rbN, rab; /*received and expected bits*/ do :: in?rb1,rbN,rab,d; delay(xk, TD); if :: skip; out!rb1,rbN,rab,d; :: skip; fi; delay(xk, 1); od; } proctype L(chan in, out) { timer xl; do :: in?ack; delay(xl,TD); if :: skip; out!ack; :: skip; fi; delay(xl,1); od; } /*The Properties 1 trough 8 of Subsection 6.3 can be verified using assertions enclosed in a monitor process. For Prop. 9 and 10 the SClient and RClient should be changed in a manner analogous to the one in the UPPAAL specification. Note that we have to put the assertion followed by a delay in a loop so that it can be executed over an over again for each time slice. Because we need a new timer for the monitor the corresponding lines for timer declaration, shutoff macro, __Timers() process and init process (the last one is not essential) should be changed appropriately. Of course, a classical never claim for []p could also be used*/ /*proctype Monitor() { do ::*/ /*assert(!File[4]@same || !(SClient[5]@ok && RClient[6]@nok));*/ /*1*/ /*assert(!File[4]@same || !(SClient[5]@nok && RClient[6]@ok)); */ /*2*/ /*assert(!(File[4]@other && SClient[5]@ok)); */ /*3*/ /*assert(!(SClient[5]@ok || SClient[5]@nok || SClient[5]@dk) || (Sender[2]@idle || Sender[2]@error));*/ /*4*/ /*assert(!(Sender[2]@idle || Sender[2]@error) || !SClient[5]@file_req);*/ /*5*/ /*assert(!Receiver[3]@new_file || (RClient[6]@ok || RClient[6]@nok));*/ /*6*/ /*assert(!RClient[6]@nok)*/ /*if n=1*/ /*7*/ /*assert(!SClient[5]@nok);*/ /*if n=1*/ /*8*/ /*delay(cm, 1); od; }*/ init { atomic{ /*in the beginning all the timers are switched off*/ run Sender(B, F); run K(F, G); run L(A, B); run Receiver(G, A); run File(SCtoF, RCtoF); run SClient(SCtoF); run RClient(RCtoF); /*run Monitor();*/ }; }