Application of Coloured Petri Nets to Protocols
Jonathan Billington, University of South Australia, Australia
Lars Kristensen, University of Aarhus, Denmark
Abstract
The specification and development of communication protocols is a
challenging task. This is due to protocols being inherently concurrent and
distributed. Protocols are organised into hierarchies, known as protocol
architectures (or stacks) to try to manage complexity. At each level of the
hierarchy, a protocol consists of a number of communicating concurrent
processes that provide services to distributed users, via asynchronous
message exchanges. These protocol entity processes may proceed in many
different ways depending on, for example, when user commands are received,
message arrivals from other protocol entities, timers expiring and when
processes are scheduled. The main difficulties are due to the need for
correct synchronisation of the processes and the correct delivery of the
services required in the face of communication media imperfections where
messages may be lost, duplicated, delayed and delivered out of sequence.
This complex behaviour makes the design of correct protocols difficult.
This has motivated the use of formal description techniques and supporting
computer tools for
the specification, analysis, verification and testing of protocols.
In this tutorial we focus on the application of Coloured Petri Nets for
modelling, analysis and verification of communication protocols. The tutorial
provides an introduction to the application domain of communication
protocols, identifying the key activities and goals in protocol
engineering and how these can be supported by CP-nets, their analysis
methods and supporting computer tools. The tutorial will illustrate
the application of CP-nets using a number of recent case studies applying
CPN modelling and analysis to protocols from the Internet
protocol suite, such as the Transmission Control Protocol and the Internet
Open Trading Protocol. The tutorial will also present
examples of CPN modelling and analysis conducted in a recent protocol
development project with Ericsson Telebit A/S, illustrating the
practical use of CP-nets in an industrial protocol development process. The
industrial perspective on this approach will also be presented.
Last modified: Mon Feb 23 16:32:18 2004