In: Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003), Eindhoven, The Netherlands, June 23-27, 2003, pages 377-396. Volume 2679 of Lecture Notes in Computer Science / Wil M. P. van der Aalst and Eike Best (Eds.) --- Springer-Verlag, June 2003.
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.
Back to the Petri Nets Bibliography