Generation of a Service Language for the Resource Reservation Protocol Using Formal Methods

摘要

The Resource Reservation Protocol (RSVP) is a signalling protocol, which transports and maintains Quality of Service (QoS) information along the path of a data flow. It is being modelled and analysed using a verification methodology proposed by (Billington et al 1986). The methodology includes a service and protocol specification. This paper is focused on the definition, modelling, and analysis of the RSVP service specification. A service language including all the possible service primitives sequences was also generated. It is being used as part of the verification process of RSVP. Also, this service specification will allow other resource reservation protocols to be developed that satisfy this service.