Analysing properties of the resource reservation protocol

Abstract

The goal of the Resource Reservation Protocol (RSVP) is to establish Quality of Service information within routers and host computers of the Internet. This paper describes a model of RSVP and presents the analysis approach and results. A large part of RSVP is modelled using Coloured Petri Nets. The model provides a clear, unambiguous and precise definition of the considered features of RSVP, which is missing in the current protocol specification. The model is analysed for a set of general properties, such as correct termination, and a set of RSVP specific properties defined in this paper. The properties are checked by querying the state graph and its associated strongly connected component graph. As a first step, we analyse RSVP under the assumption of a perfect medium to ensure that protocol errors are not hidden by rare events of the medium. The results show that the RSVP model satisfies the defined properties. © Springer-Verlag Berlin Heidelberg 2003.