Affiliations: Computer Systems Engineering Centre, School of
Electrical and Information Engineering, University of South Australia, Mawson
Lakes, SA 5095, Australia. E-mail: j.billington@unisa.edu.au | 224 Leicester Street Carlton, Victoria 3053, Australia
Abstract: The TCP/IP protocol suite defines the procedures governing the
movement of data within the Internet. A major component of the suite is the
Transmission Control Protocol (TCP), which ensures data flows reliably between
Internet applications. We use Coloured Petri Nets (CPNs) to model the
application's view of the service provided by TCP for the transfer
of data. This service depends on the storage capacity available in the
Internet. We firstly establish exact expressions for the size of the CPN
model's reachability graph (or state space) in terms of the storage
capacity. They indicate that both the nodes and arcs of the state space grow
exponentially in the storage capacity. Secondly,we derive a symbolic state
space which represents an infinite family of state spaces, one for each value
of the capacity. We prove that each member of this family is a strongly
connected graph and that its associated finite state automaton is deterministic
and minimum. Finally, we formulate the TCP data transfer service language for
arbitrary capacity, from the symbolic representation of the family of automata.
This service language is the yardstick against which the TCP data transfer
protocol can be verified with respect to user observable sequences of events.
Keywords: TCP, Data Transfer Service, Service Language, Parametric Systems, Symbolic Automata, Coloured Petri Nets
