25 - 29 de Noviembre de 2002

Montevideo, Uruguay

Radisson Victoria Plaza Hotel

 
CL26
 
Techniques and Tools for Formalising and Analysing the Resource Reservation Protocol: A Coloured Petri Net Approach

María E. Villapol
School of Computer Sciences, Central University of Venezuela
mvillap@strix.ciens.ucv.ve
Jonathan Billington
Computer Systems Engineering Centre, University of South Australia
j.billington@unisa.edu.au
 
Abstract

The goal of the Resource Reservation Protocol (RSVP) is to establish Quality of Service information in the form of resource reservations (such as buffers and bandwidth) within routers and host computers of the Internet. It is intended to support emerging Internet applications that require performance guarantees. Currently, Internet protocols are not formally specified when they are developed. Instead they are described in a narrative way in documents called Request for Comments (RFCs). This is the case for RSVP. To increase confidence in RSVP we have formalised and analysed its narrative specification using Coloured Petri Nets (CPNs). This paper demonstrates how CPNs can be used for modelling and analysing RSVP. Among the several beneficial features of CPNs are: graphical facilities for specification; support for different levels of abstraction; hierarchical structuring mechanisms; and verification and validation methods, such querying the state space to investigate properties, and language equivalence to check the consistency of different levels of abstraction. These facilities allow us to create a model, that provides a clear, unambiguous and precise definition of RSVP, and to analyse the protocol for functional correctness. The paper concentrates on the approach and the tools used in this investigation.

Keywords: RSVP, Quality of Service (QoS), Coloured Petri Nets, State Spaces



Volver

infoUYclei 2002