Example of a communication protocol : Analysis of TCP

Presentation of TCP

TCP is an old protocol, originally defined in 1981. Its purpose is to provide connections for reliable communication between processes running in different computers connected to the Internet which provides the IP packet transmission service which is not reliable (packets may get lost or be received out of sequence - or even dublicated). The system architecture for TCP is the typical architecture of any communication protocol shown in figure (a). Figure (b) shows the black-box view of the TCP system which provides the reliable communication service to the users. For simplicity, this figure shows only two ports through which the application processes in the different computers access the reliable communication service. These ports are also called service access points (SAP).

architecture

TCP is a quite complex protocol, especilly considering all the extensions that have been added over time. In the following, we take a very abstract view, considering only the first phase of the protocol during which the logical connection is established between the two communicating users on the different computers. We consider the interactions that occur until the connected state is reached where data is exchanged between the two parties (data exchange is not modelled in what follows).

The establishment of a TCP connection is based on a so-called three-way handshake involving three messages. In fact, one assumes that both parties must send a sync message which proposes a sequence number for data exchange which must be followed by an acknowledge message from the other side. This leads typically to the following sequence diagram (a). (The second message includes an acknowledgement and also the sync from the second party).

TCP

Definition of the communication service provided by TCP

When TCP was developed, people concentrated on the white-box view (defining the rules for message exchanges between the two protocol entities), because the notion of communication service provided by the black-box view was not yet well established. In my paper of 1980, the black-box service view was high-lighted for the first time. In the early 1980ies, the OSI standardization gave rise to typical service specifications for the establishement of a connection as shown above in sequence diageram (b). It involves a Request at the initiator side, followed by an Indication at the other side, followed by a positive Response at the other side (if the user accepts this connection), and followed finally by a Confirmation at the initiator side. This is similar to the service interactions of a telephone system when a connection is established between user A and B: A.activate-phone, A. dial-number, B.ring, A.hear-ringing, B.activate-phone, both.talk.

The above service specification involves inputs and outputs between the user and the protocol entity. These interactions are normally called service primitives. This is natural for system modeling based on state machines. It is a somehow symmetric interface.

However, the designers of TCP where programmers that were not used to adopt more abstract modeling approaches, simply using what their programming language provided. What typical programming languages provide are Appication Programming Interfaces (API) in the form of a set of methods that can be called. This lead to the so-called "socket interface" for TCP (which you have seen in Java). Here the application has to decide whether it will make a connection (calling the connect method), or receiving a connection (calling the listen method). The method interface is not symmetric between the calling and called side.

Definition of the TCP protocol

The method names of the TCP socket interface have been included in the state machine model of the TCP protocol, as shown by the state machine model from Wikipedia:

TCP

Using LTSA to analyse the TCP protocol

Simplified version

We start out with a simplied version where user A makes the request for establishing a TCP connection with user B. Using the sequence diagram (a) above, and following the vertical time lines, one can derive a sequence of send and receive operations to be performed by the initiating and responding sides. These operation sequences can be modeled as two state machines for the initiating and responding protocol entities. This gives then rise to the LTSA model in file TCP simplified.lts (please have a look using LTSA). The protocol entity representing user A is the initiator and B is the responder. By composing the SYSTEM, LTSA makes the reachability analysis and finds that there is no deadlock. We have also defined a property TCP_SERVICE which is the abstract view at the black-box level, which says that dataExchange can only occur after Listen and Connect have occurred (in any order). By composing Check_Service, LTSA checks that this property actually holds for the given system specification.

Symmetric version

The design of TCP allows for the case that both users A and B can request a connection to the other side, possibly at the same time.

Using a more evoled service interface ... (see lab-4)


Course notes - Gregor v. Bochmann - University of Ottawa. Created January 20, 2015; revised February 3