VU University Amsterdam (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
3,296,792 states and 11,010,169 transitions.
The Transmission Control Protocol (TCP) plays an important role in the
Internet, providing reliable transport of messages through a possibly
faulty medium to many of its applications. TCP enables two parties to
reliably communicate over a faulty network. Its responsibilities can
roughly be divided into two categories: Connection management
sets up the connections, manages the connection states and ensures that
connections are closed in a safe manner; Data transmission
involves the transfer of segments from the sender to the receiver.
TCP uses the Sliding Window Protocol for its data transfer. Both sender and receiver maintain a window of n sequence numbers, ranging from 0 to n-1, from which they can send or where they can receive data items. The sender may send as many bytes as the size of its window before it has to wait for an acknowledgement from the receiver. Once the receiver sends an acknowledgement for m bytes, its window slides forward m sequence numbers. Likewise, the sender's window slides m sequence numbers if this acknowledgement arrives.
The performance of TCP is directly influenced by the size of the send window: the larger it is, the more data a sender can send without having to wait for an acknowledgement. If the medium can hold more than the window size, unnecessary delay will be introduced into the communication due to the restriction on the window size. To resolve this issue, RFC 1323 proposes the Window Scale Option (WSO). If implemented, the send and receive windows are maintained as 32-bit numbers. Whenever an entity receives an acknowledgement, it applies the scale factor to the window size the before it updates its send window. Likewise, whenever an entity sends an acknowledgement it sets the window field of the outgoing segment to the size of its receive window.
The goal of this case-study was to verify that the TCP continues to function correctly in presence of the WSO. To this purpose, TCP was formally specified in μCRL, including the Data Transfer and Connection Teardown phases as specified in RFCs 793 and 1122, extended to include the WSO, as specified in RFC1 323. The LTS model was generated using the LTSmin toolset, and two properties regarding the successful completion of TCP connections were specified in regular alternation-free μ-calculus and checked on the LTS using the EVALUATOR model checker of CADP.
The TCP protocol is complex and its specification consists of many
documents that mainly describe the proposed functioning of the protocol
in natural language. A formal specification provides a more precise
reference of the intended function of a protocol, and also a useful
basis for formal verification.
L. Lockefeer, D. M. Williams, and W. Fokkink.
"Formal Specification and Verification of TCP Extended with the
Window Scale Option".
Science of Computer Programming 118:3-23, March 2016.
Available on-line from https://doi.org/10.1016/j.scico.2015.08.005
Vrije Universiteit Amsterdam
Faculty of Sciences
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081
1081 HV Amsterdam
Tel: +31 20 598 7735
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|