The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.