Formal Specification and Analysis of the Resource Reservation Protocol

摘要

This thesis explores the practicality of using the Resource ReSerVation Protocol (RSVP) model to prove quality of service guarantees over networks. An overview of the requirements to provide quality of service is provided. Using Finite State Machine analysis, the RSVP protocol is formally specified and found to be suitable for reserving resources along a proposed path. However, the distributed nature of the RSVP model and its reliance on quality of service aware routing protocols is problematic. Several examples where RSVP provides less than optimal and/or incorrect results are studied. The framework for alternate model of proving quality of service is proved. This model uses a centralized server for flow path computation. The server-based approach provides more accurate results than the RSVP model and is capable of network optimization; yet it places fewer strains on network resources and appears easier to implement.