TReX Examples

The Bounded Retransmission Protocol


Description of the example

Specification of the service

The Bounded Retransmission Protocol (BRP) is a data link protocol used by Philips. The service it delivers is to transfer in a reliable manner, if possible, large files (sequence of data of arbitrary length) from a sender to a receiver. Each file is sent in a separate frame. Both sender and receiver obtain indication about the state of the transfer done.

More precisely, at the sender side, the protocol receives the file in the form of a sequence of datum s = d1, ..., dn by repeatedly calling action REQ. At the end of the transfer, it sends to its client one of indications:

At the receiver side, the protocol delivers each datum received correctly with one of the following indications:

The properties the service should satisfy (safety) are the following:

  1. each file received by the sender (using REQ) must be followed by an indication (one of SOK, SNOK, or SDNK) to the sender's client before the asking for a new reception.
  2. indication RFST must be followed by one of the two indications ROK or RNOK before the beginning of the transfer for a new file (new request of a sender)
  3. indication SOK at sender must be preceded by indication ROK at receiver.
  4. indications sent by the sender and receiver must match, i.e., SOK with ROK, SNOK and SDNK with RNOK
These properties may be resumed by the following automaton.

Description of the protocol

The BRP is an extension of the Alternating Bit Protocol (ABP). Indeed, it is a (partially) reliable transfer protocol using positive acknowledgements and stop-and-wait approach (i.e., the additional information sent with data messages is only one bit). Unlike ABP, BRP deals with sequence numbers of datum in the file and interrupts transfer after fixed number of retransmissions for a datum.

The protocol consists of two parts, the sender S and the receiver R, that communicate through two lossy fifo channels M (for sending of datum messages) and A (for sending of acknowledgement messages). Since the channels are lossy fifo, messages are either lost or arrive in the order they are sent.

Data messages sent from the sender S to the receiver R through the channel M have the following structure: (first, last, toggle, datum) where to the datum are added three bits:

Acknowledgement messages sent from R to S trough A have a similar structure (first, last, toggle), where datum is not present.

The behaviour of S and R is the following.
The sender S starts by reading (action REQ) the file in the form of the sequence of datum s = d1, ...,dn (with n >= 2 since the case n=1 is equivalent to ABP). Then S sends to R through M the first data frame (1, 0, 0, d1), and waits for the acknowledgement.
Let us consider first the ideal case where frames are never lost. When R receives the data frame from S, it delivers to his client the data datum d1 with the indication RFST, and sends to S an acknowledgement frame (1, 0, 0) through the channel A. When S receives this acknowledgement, it sends to R the second frame (0,0,1,d2). After reception of this frame, R delivers d2 with the indication RINC, and sends the acknowledgement (0,0,1) to S. Then, the next frame sent by S (if n >= 4) is (0, 0, 0, d3), and the sequence of actions above is repeated until the last frame (0,1,togglen,dn) is sent. When R receives the last frame, it delivers dn with the indication ROK, and acknowledges its receipt. The sender S communicates to its client the indication SOK.

Now let us consider the case where frames are lost.
To detect losses, when S sends a datum message it starts a timer of timeout Ts. A datum message is considered lost if its acknowledgement does not arrive before expiration of Ts (a parameter of the protocol). In this case, the sender retransmits the same message and restarts the timer. However, it does retransmissions only up to a fixed maximal number MAX (a parameter of the protocol). So, the sender has to maintain a counter rc of retransmissions done for a datum message, which is initialized to zero each time a new datum is sent and it is incremented at each retransmission of this datum. When rc reaches the MAX, the sender stops the transfer of the file and concludes that the connexion with the receiver is broken. Then, it informs his client that a failure occurred by one of the two indications: SNOK if the datum not acknowledged is not the last, or SDNK if it is the last one.
On the receiver's side, the delay between two message arrivals are measured using another timer of timeout Tr (a parameter of the protocol). When R receives a message, it resets the timer. If the frame is new (according to the toggle bit), it delivers the datum with the corresponding indication, otherwise it resends the last acknowledgement message. If the timer expires, R concludes that the connexion with the sender is broken and delivers the indication RNOK to its client.

In the protocol, two assumptions are made on the behaviour of S and R:

Two abstract models

Lossy Channel System

In this abstract model, we take into account only the communication between sender and receiver through the unreliable, fifo channels.

More precisely, we have made the following abstractions:

Since the control of the BRP does not depend on the content of the file, we abstract the datum sent in data messages, and only information first, last, toggle is considered in data messages. Moreover, we represent this information in a compressed form, such that the messages sent through channel M belongs to the finite alphabet Msg = {fst, last, 0, 1}, where:
Size of files
Since it is only relevant to know whether a frame is the first one, the last one, or an intermediate one, we abstract the size of file (n), and we consider that n>=2, chosen nondeterministically by the sender.
We abstract the real-time behaviour of the protocol, by considering that the sender and the receiver decide nondeterministically when timeouts occur, provided that their corresponding input channels are empty (we use channel emptiness testing).
Number of retransmissions
We abstract the counter rc and the parameter MAX by the following (predicate abstraction) technique. The only relevant information w.r.t. rc and MAX is whether rc < MAX or rc >= MAX. Then, we consider that the sender chooses nondeterministically when the maximal number of retransmissions is reached to abort transmission. This means that the size of the channel M is unbound, which implies that the size of A is unbound too.
Due to the nondeterministic choice, the value of MAX may change for each transmission in this abstract model. This means that this model is an abstraction of the whole family of BRP for arbitrary fixed values of MAX.
Assumptions A1 and A2
Since our model is untimed, we cannot implement A1 and A2 using real-time constraints on timeouts. Instead, we use boolean shared variables to synchronise the sender and the receiver. We consider the two following variables:

The abstract model obtained for BRP is a lossy channel system given by the following automata.

Go to analysis results obtained with TReX

Parametric Timed Counter Lossy Channel System

This abstract model is the most general that can be dealt by TReX. It abstracts only features of the protocol which are not relevant to the control part and that can be dealt by TReX.

We have made the following abstractions:

For the same reason than in the previous model, we abstract the datum values. We consider the following finite alphabet for the messages sent Msg = {fst0, fst1, last0, last1}. This alphabet corresponds to files with two datum, each datum being toogled.
Size of files
As explained above, we consider only files built from two datum, i.e., n=2. This restriction is needed to be able to obtain results with TReX in reasonable time and space.

The following design choices are used:

No abstraction is done on the real-time constraints. We use clocks to model the two timeouts of (parameter) delays Ts and Tr.
Number of retransmissions
No abstraction is done on the retransmission. We use a counter rc which counts the retransmissions y the sender and an integer parameter MAX to limit the progress of rc. Then, the value of MAX is then fixed for a reachable configurations path.
Assumptions A1 and A2
To ensure these assumptions, we give the following initial constraints on parameters MAX, Ts, Tr:
MAX >= 2  and  Tr > 2*MAX*Ts  and  Synch > Tr  and  Tr > 0  and  Ts > 0
where Synch is the time elapsed between the abortion of a transfer and the beginning of a new transfer.

The abstract model obtained for BRP is a parameterized timed extended automata with lossy channels given by the following automata

[sender] [receiver]

Go to analysis results obtained with TReX

Experimental results

The following table resumes the results obtained by applying TReX to this two abstract models. The experiments have been done on a Ultra Sparc 10.
Model Memory
Lossy channels system 6.3 0.10 brp_lcs.scf brp_lcs.aut
Param. Extended Autom. 806 5026 brp_pcclcs.scf brp_pcclcs.aut

Related papers