Architecture of the protocol
Definition of the protocol
The BRP protocol is a variant of the alternating bit protocol, where not single messages, but packages of arbitrary length are transmitted and the number of possible retransmissions per message is bounded by some number max. We consider a fully parameterized version of the protocol where the packages can be of any size, and max any positive number.Each package contains an arbitrary number of messages. There are three possible confirmations that the sender may deliver to its client at the end of the transmission phase: OK if all messages have been transmitted and acknowledged, NOT_OK if the transmission has been aborted because more than max retransmissions would have been necessary to deliver a message, DONT_KNOW if the last message has not been acknowledged (in this case it is not possible to know if this message or its acknowledgment has been lost).
The receiver acknowledges each received message, and delivers an indication to the receiving client. The indication is FIRST for the first received message of a package, INCOMPLETE for any intermediate message, and OK for the last message of the package. In the case that the sender abandons the transmission of a package after sending successfully at least one message, the receiver delivers a not NOT_OK indication.
There are two timers T1 and T2. Timeout of T1 indicates to the sender that a message (or its acknowledgment) has been lost. Timeout of T2 indicates to the receiver that the sender has definitively abandoned the transmission of the package.
The protocol is described in a syntax close to the Dijkstra guarded command language with explicit control. The system consist in the parallel composition of a sender, a receiver and the environment (loss of messages). The channels are not represented as processes, but just as shared variables. L_IN and L_OUT are respectively the list of acknowledged and received messages.
We consider only packages of messages with at least 3 messages, in order to have the three possible indication: FIRST,INCOMPLETE and OK.
The channels are not represented as processes, but just as shared variables.
Abstract state graph definition
The following predicates are used to define the abstract state graph:{timer3 ; ctoggle ; ftoggle ; first ; ffirst ; flast ; busy ; rn=max ; rn < max ; flagm ; flagack ; timer1 ; timer2 ; timer3_enable ; proj_2(Cm) ; rtoggle ; stoggle ; length(L) > 1 ; length(L)=1 }
Generation of the Abstract State graph
The generated abstract state graph contains 475 states and 685 transitions. Only the following global control configurations are reachable:{ (1 1 1) ; (2 1 1) ; (2 2 1) ; (3 1 1) ; (5 1 1) ; (6 1 1) ; (2 4 1) ; (6 3 1) ; (4 1 1) }
Verification of the protocol
Correctness criterion:
We want to prove that for each package, the indication and the confirmation delivered to the clients are consistent. That means, if the sender delivers a OK confirmation, the receiver delivers an OK indication. If the receiver delivers a NOT_OK indication, the sender delivers the DONT_KNOW or NOT_OK confirmation. These properties can easily be expressed by temporal logic formulae.By hiding all the transition which does not concern the external behavior of the protocol, and by reducing modulo observational equivalence we obtain the following state graph. It is easy to see that on this reduced graph all the required properties are verified
