Affiliations: Computer Systems Engineering Centre, University of
South Australia. jonathan.billington@unisa.edu.au | School of Telecommunication Engineering, Suranaree
University of Technology, Thailand
Note: [] Address for correspondence: Computer Systems Engineering Centre,
University of South Australia, Mawson Lakes, SA, 5095, Australia
Abstract: 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.
Keywords: Internet Protocols, DCCP, Coloured Petri Nets, Formal Specification, Evolutionary Modelling
