The Resource Reservation Protocol (RSVP) is one of the proposals of the Internet Engineering Task Force (IETF) for conveying Quality of Service (QoS) related information in the form of resource reservations along the communication path. The RSVP specification (i.e. Request for Comments 2205) provides a narrative description of the protocol without any use of formal techniques. Thus, some parts of the document may be ambiguous, difficult to understand, and imprecise. So far, RSVP implementations have provided the only mechanism for validating. The cost for fixing errors in the protocol found in the implementation can be high. These disadvantages together with the fact that RSVP is complex make it a good target for formal specification and verification. This thesis formally defines the RSVP Service Specification, models RSVP using a formal method known as Coloured Petri Nets (CPNs) and attempts to verify the model. The following steps summarise the verification process of RSVP. Firstly, the RSVP service specification is derived from the protocol description and modelled using CPNs. After validating the model, the service language, which defines all the possible service primitive occurrence sequences, is generated from the state space of the model by using automata reduction techniques that preserve sequences. Secondly, RSVP is modelled using CPNs. The model is analysed for a set of behavioural properties. They include general properties of protocols, such as correct termination, and a set of new properties defined in this thesis, which are particular to RSVP. The analysis is based on the state space method. The properties are checked by querying the state graph and checking reachability among multiple nodes of its associated Strongly Connected Component (SCC) graph. As a first step, we analyse RSVP under the assumption of a perfect medium (no loss or duplication) to ensure that protocol errors are not hidden by rare events of the medium. The state space is reduced to obtain the sequences of service primitives allowed by RSVP known as the protocol language. Then, the protocol language is compared with the service language to determine if they are equivalent. The desired properties of RSVP are proved to be satisfied by the RSVP CPN model, so that the features of RSVP included in the CPN model operate as expected under our modelling and analysis assumptions. Also, the language analysis results show that RSVP service primitive occurrence sequences generated by the RSVP model are included in the proposed model of the service specification. However, some service primitive occurrence sequences generated from the service specification model are not in the protocol language. These sequences were analysed. There is strong evidence to suggest that these sequences would also appear in the protocol if the capacity of the medium in the RSVP model was marginally increased. Unfortunately, the standard reachability analysis tools would not handle this case, due to state space explosion. / Thesis (PhD)--University of South Australia, 2003

Thesis (M.S.)--University of Missouri--Rolla, 2007. / Vita. The entire thesis text is included in file. Title from title screen of thesis/dissertation PDF file (viewed March 27, 2008) Includes bibliographical references (p. 55-56).

Thesis (M.S.)--Brigham Young University. Dept. of Computer Science, 2006. / Includes bibliographical references (p. 199-200).

Thesis (Ph. D.)--School Computing and Engineering. University of Missouri--Kansas City, 2006. / "A dissertation in computer networking and software architecture." Advisor: Lein Harn. Typescript. Vita. Title from "catalog record" of the print edition Description based on contents viewed Nov. 13, 2007. Includes bibliographical references (leaves 203-214). Online version of the print edition.

Thesis (M.S.)--University of Missouri--Rolla, 2007. / Vita. The entire thesis text is included in file. Title from title screen of thesis/dissertation PDF file (viewed April 21, 2008) Includes bibliographical references (p. 48).

Thesis (Ph.D.)--University of Waikato, 2007. / Title from PDF cover (viewed February 29, 2008) Includes bibliographical references (p. 149-160)

Diss. (sammanfattning) Uppsala : Uppsala universitet, 2005. / Härtill 6 uppsatser.

Thesis (Ph.D.)--University of Melbourne, Dept. of Computer Science and Software Engineering, 2006. / Typescript. Includes bibliographical references (leaves 260-271).

Thesis (M.S.)--State University of New York at Binghamton, Department of Computer Science, Thomas J. Watson School of Engineering and Applied Science, 2007. / Includes bibliographical references.

Thesis (M.Eng.) - Carleton University, 2002. / Includes bibliographical references (p. 90-92). Also available in electronic format on the Internet.