Formal specification of the TCP service and verification of TCP connection management
Files
(Published version)
Date
2004
Authors
Han, Bing
Editors
Advisors
Journal Title
Journal ISSN
Volume Title
Type:
thesis
Citation
Statement of Responsibility
Conference Name
Abstract
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.
School/Discipline
School of Electrical and Information Engineering
Dissertation Note
Thesis (PhDComputerSystemsEng)--University of South Australia, 2004.
Provenance
Copyright 2004 Bing Han
Description
eng
Access Status
506 0#$fstar $2Unrestricted online access