Formal Verification of T/TCP

Mark Smith, AT&T Labs-Research

TCP works well for data streaming, but does not work well for transactions because the synchronization overhead makes it inefficient for short connections. A transaction is typically a sequence of two messages -- a request and a response. T/TCP is an experimental TCP/IP transport level protocol which is designed to provide the same service as TCP, but with optimizations to make it efficient for transactions. However, this protocol does not provide the same service as TCP as it may deliver the same message twice in some situations. Even though the service provided by T/TCP is not exactly the same as TCP, its behavior may be acceptable for some applications. Therefore, we define a specification that captures this behavior of T/TCP while maintaining the other correctness properties of TCP. We then verify that T/TCP satisfies this specification.

We formally present the specification and the protocol using I/O automaton models. The formal verification is done using invariant assertion and simulation techniques.