TReX Examples

The Bounded Retransmission Protocol

• Description of the example
• Specification of the service
• Description of the protocol
• Two abstract models
• Lossy channel system
• Parametric Timed Counter Lossy Channel System
• Experimental results
• Related papers

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:

• SOK if the hole file has been transferred successfully,
• SNOK if the file has not been transferred completely,
• SDNK if the file has been transferred successfully except for its last datum which correct transfer has not been confirmed.

• RFST if it is the first datum of the file and more data will follow,
• RINC if the datum is neither the first or the last one,
• ROK if the datum is the last one, so the transfer of the file is completed,
• RNOK if the connexion with the sender is broken; the datum sent with this indication is not relevant.

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

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:

• first and last indicate whether the datum is the first or the last one in the considered file,
• toggle is an alternating bit used by the stop-and-wait protocol to detect duplications in transmission; it is initialized to 0 at the beginning of the transfer of each file.

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:

• A1: R does not conclude prematurely that the connexion with S is broken.
  This means that the delay Tr must be large enough to allow MAX retransmissions of a frame.
• A2: If S concludes that the connexion with R is broken, it waits before starting a new file transfer in order to allow R to detect also the abortion of the transfer for the current file.
  This means that S must wait enough time after abortion to be sure that the delay Tr has expired at R.

More precisely, we have made the following abstractions:

Frames

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:

• fst and last represent the first resp. the last data message, and
• 0 and 1 represent the intermediate data messages by their toggle bit.

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.

Timeouts

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:

• abort informs the receiver about the decision of the sender to abort the transfer,
• rtrans informs the sender that the receiver sent the indication of the end of the transfer to its client (using indications ROK or RNOK).

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

Go to analysis results obtained with TReX

We have made the following abstractions:

Frames

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:

Timeouts

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

Go to analysis results obtained with TReX

• P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. Proceedings of TACAS'99, number 1579 in LNCS.
• A. Annichini, E. Asarin, and A. Bouajjani. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. Proceedings of CAV 2000, (C) Springer-Verlag, volume 1855 of LNCS, pages 419-434.