Multimedia Services in Open Distributed Telecommunications Environments

The design and analysis of transport protocols for reliable communications constitutes the topic of this dissertation. These transport protocols guarantee the sequenced and complete delivery of user data over networks which may lose, duplicate and reorder packets. Reliable transport services are required by a wide range of applications such as the World-Wide Web, remote network access, and distributed computing. The design of these protocols is heavily influenced by the parameters of the underlying network infrastructure and by the assumptions about the host computers and applications. Therefore the recent advances in optical transmission and computer technologies stimulated the design of several novel transport protocols. Many of the proposed protocols use similar or at least related techniques. Our goal with this thesis is to improve the understanding of reliable communications by analyzing the protocols that implement this service and to contribute to the design of reliable transport protocols. The basis of our analysis is the formal specication and verication of the protocol mechanisms under investigation. The behavior of the protocol is captured by a state-transition system and properties are established using assertional reasoning. The framework is capable to handle unbounded and modulo-N state variables and to capture real-time aspects of the protocols which is essential for the modeling of realistic systems. Practical protocols of considerable complexity are specied and veried in the thesis. One advantage of the formal verication is that it increases our condence in the correctness of these protocols. The formalism forces us to clarify all the details of the working of the protocol and to state explicitly every assumption about the protocol and its environment. During the process of the verication one also gains insight into the mechanisms of the protocol. But probably the most important result is that during the verication we obtain conditions for the correctness of the protocol in the form of inequalities on some protocol parameters. These conditions allow the comparison of the dierent protocol mechanisms and can be used to judge the suitability of a protocol for a certain environment. The functionality of transport protocols can be naturally divided into data transfer and connection management. Data transfer deals with the sequenced delivery of user data, while connection management is concerned with the orderly setup and release of connections. In the thesis we study three dierent data transfer protocols. The usage of timestamps in data transfer protocols is analyzed in detail through the example of the PAWS mechanism which was proposed as an extension to TCP. The analysis reveals that the use of timestamps increases the functionality of the transport protocol by facilitating the simple measurement of round-trip delays, but it also reduces the maximum allowable transmission rate as compared to the plain sliding-window protocol. Another data transfer protocol called SNR is analyzed which is based on the idea of periodic state exchange. We start from an earlier specication of SNR and compare it to the plain sliding-window protocol. The analysis reveals that the maximum transmission speed achievable by that SNR specication is higher than that of the plain sliding-window protocol, but it comes with a serious limitation. In the SNR specication it is assumed that no duplicates are generated by either the network or the transport protocol itself. This assumption may seriously limit the eective performance of the protocol in case of losses in the network and demonstrates the importance of considering all the assumptions when selecting a protocol for a certain environment. The use of timestamps is also investigated in the context of connection management protocols. The detailed analysis of the connection setup protocol SCMP is presented which is based on the assumption that clocks of computers can be synchronized relatively cheaply even in a large network. In our verication it is proven that the safety of the protocol does not depend of the synchronization assumption, therefore the protocol can be used safely in cases when there are no absolute guarantees of the clocks being synchronized. Since practical clock synchronization algorithms give only probabilistic guarantees, our result provides an important theoretical support of the applicability of the protocol in practical environments. Based on earlier work by others, a family of connection management protocols is analyzed that use a cache to store information needed to shorten the connection setup latency. We contribute to this work by proposing improvements which allow to reduce considerably the memory usage of these protocols. Furthermore, we show that the correctness of the protocol can be assured without assuming an upper bound on the incarnation lifetime, i.e., the maximum duration of a connection. This result greatly improves the practical applicability of the protocol