Using the approach of Coloured Petri nets (CPNs) and automata theory, this thesis shows how to formalise the service provided by the Transmission Control Protocol (TCP) and verify TCP Connection Management, an essential part of TCP. Most of the previous work on modelling and analysing TCP Connection Management is based on early versions of TCP, which are different from the current TCP specification. Also the scope is mainly confined to the connection establishment procedure, while the release procedure is either simplified or omitted from investigation. This thesis extends prior work by verifying a detailed model of TCP Connection Management. In defining the TCP service, the set of service primitives and their sequencing constraints are specified at each service access point. / Thesis (PhDComputerSystemsEng)--University of South Australia, 2004.
| Identifer | oai:union.ndltd.org:ADTP/267564 |
| Creators | Han, Bing. |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Rights | copyright under review |
Page generated in 0.002 seconds