PhD Thesis

I began my PhD candidature in February 1998 and submitted my thesis for examination in August 2001. All three international examiners passed the thesis, without a need for revision. My degree was awarded on 18 December 2002.Photo of Steven Gordon's PhD certificate

My thesis was titled Verification of the WAP Transaction Layer using Coloured Petri nets. The summary of the thesis is given below, or alternatively you may download the complete thesis in PostScript (690kb) or PDF (1.25Mb) form. There is an errata available for this thesis. If you have any questions about the work, or require some of the models, please contact me. Update (20 Feb 2012): you can now download and compile the LaTeX source for my thesis.

Verification of the WAP Transaction Layer using Coloured Petri nets

The rapid growth of the Internet and its use has inevitably led to its entrance into the wireless world. However, the characteristics of wireless networks and the devices typically used in them, result in a significantly different operating environment than that provided by the existing Internet infrastructure. A range of protocols and architectures, of which the Wireless Application Protocol (WAP) is one, have been proposed to overcome the difficulties of providing Internet services in wireless networks. The Transaction layer in WAP defines a protocol to support transactions where an Initiator makes a request to a Responder, which returns the requested information. This thesis applies a protocol engineering methodology to analyse the functional behaviour of the Transaction layer in WAP. Coloured Petri net (CPN) models of the Class 2 Transaction layer service (TR-Service) and protocol (TR-Protocol) are created based on an existing specification. The aim is to verify that the TR-Protocol is a faithful refinement of the TR-Service, in terms of sequences of primitives seen by the users.

The WAP Transaction layer specification defines the TR-Service using narrative descriptions and a table specifying the possible primitives that may follow one another, as seen by a user. The CPN modelling and analysis process has revealed the existing specification is ambiguous and incomplete. A set of rules is defined to remove the ambiguities. These rules, and the existing specification, are formalised in the TR-Service CPN. State space generation and automata reduction are used to produce the TR-Service language, the set of possible global sequences of primitives, as opposed to the local sequences only available in the WAP specification.

The WAP Transaction layer specification also describes the TR-Protocol. The dynamic behaviour of the TR-Protocol is described mainly using state tables. These state tables are formalised by the creation of the TR-Protocol CPN. Without loss of generality, only a single transaction between one Initiator and one Responder is modelled. As the initial focus is on the core operation of the TR-Protocol, the version handling and segmentation and re-assembly features are omitted from the model. The underlying service (the Transport layer in WAP) is assumed to be error free (no corruption, loss or duplication), but allows overtaking of protocol data units (PDUs). A set of assumptions are also made that remove certain errors from the WAP specification. As a result, suggested changes to the specification have been input to the WAP Forum, and the majority of them have been accepted.

State space and language analysis are used to investigate the following four properties of the TR-Protocol: refinement of the TR-Service, in terms of sequences of primitives; successful termination (which includes absence of deadlocks); absence of live locks; and absence of redundant state table entries (dead transitions in the CPN). The analysis reveals the following errors in the existing specification: ambiguous semantics of two PDUs; the possibility of a re-transmitted Invoke PDU starting a new transaction from the Responder's point of view; and the possibility of the Responder misinterpreting a re-transmitted Ack PDU. A set of changes are proposed, leading to a Revised TR-Protocol. Further analysis proves the four desired properties hold for the Revised TR-Protocol for all permutations of the parameters of the CPN (i.e. a toggle of the user acknowledgment feature, and the maximum values of the re-transmission counters at both Initiator and Responder) when the counters are less than 5. This includes the suggested configuration to be used in several GSM (Global System for Mobile communication) networks.

Finally, from the results obtained from the set of parameter values analysed, observations are made on the relationship between the counters used in the TR-Protocol CPN and the state space size. These relationships may be used in the future to prove properties independently of the particular parameter values, significantly increasing the power of analysis.

Created on Wed, 18 Jan 2006, 4:14pm

Last changed on Wed, 16 May 2012, 11:58pm