One of the main objectives of the original TCP protocol is a reliable transport over wired networks. In this case the random loss of data usually occurs due to phenomena of congestion. A similar assumption is not always true in wireless networks, where the medium itself is rather prone to errors. This leads to an impaired TCP performance, a fairly undesirable behavior since it is a premier transport protocol based on the omnipresence in networking of the TCP/IP technology. Hence, various modifications ands extensions have been proposed to improve TCP performance over heterogeneous networks (aggregations of wireline and wireless links). The strategies and the mechanisms that reflect these modifications widely vary and are of different nature. The intention of the article is neither to enumerate nor to analyze the pros and cons of the these strategies, but to produce a formal model using a modeling language such as PROMELA and verify it later with SPIN, of a popular and well-known TCP modification termed as Snoop.
Both streaming techniques and wireless heterogeneous networks have recently become more widely deployed. As the current streaming techniques are primarily designed for homogenous wired networks, streaming multimedia applications in heterogeneous networks can perform poorly due to wireless networks conditions and vertical handover. These problems can significantly degrade the performance of streaming multimedia applications. Effects of the degradation are delay, jitter and packet loss resulting in lower multimedia quality. The use of some congestion recovery algorithms are detrimental factors to QoS. One approach used to control congestion in the network layer is Active Queue Management (AQM). This dissertation presents an evaluation and comparison of AQM mechanisms in heterogeneous networks. Based of the results of this research a new AQM algorithm, named the Adaptive AQM (AAQM) is proposed. The AAQM uses control law and link utilization in order to manage congestion. The action of the control law is to mark incoming packets in order to maintain the quotient between arriving and departing packets as low as possible. The AAQM enhances performance with respect to the queue length and packet loss as well as buffer space requirements. AAQM outperforms the other AQM algorithms in terms of multimedia packet loss and buffer delay.