These papers discuss sweep-line analysis of the connection management procedures of a new Internet standard, the Datagram Congestion Control Protocol (DCCP). The sweep-line method is a state exploration method which uses a notion of progress to allow states to be deleted from memory when they are no longer required. The technique shows promise but has never achieved reductions greater than about a factor of 10 in the number of states stored in memory for industrially relevant examples. These papers present a new approach for tracking progress, and they show that the peak number of states is reduced by over two orders of magnitude compared with the original progress measure for the DCCP model.
This paper specifies the connection management and synchronisation procedures of DCCP using Coloured Petri nets (CPNs). It describes how the CPN model has evolved as DCCP was being developed. The authors focus on their experience of incremental enhancement and iterative modelling in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, the paper discusses how the architecture, data structures and specification style of the model have evolved as DCCP was developed. The impact of this work on the DCCP standard is also briefly discussed.
An important characteristic of Mobile Ad Hoc Networks (MANETs) is rapidly changing topologies due to the movement of wireless mobile devices. Traditional routing approaches cannot be used in such environments. The Dynamic MANET On-demand (DYMO) routing protocol is an experimental protocol that is being designed to suit the new conditions.
This paper presents a Coloured Petri Net (CPN) model of the mandatory parts of the DYMO protocol, and shows how scenario-based state space exploration has been used to validate key properties of the protocol. The CPN modelling and verification work has had direct impact on the most recent version of the protocol specification.
This paper focuses on the route establishment procedures of the protocol. The CPN model presented in this paper contains the basic parts of the protocol and presents results from an initial state space analysis of the constructed model. Different scenarios are used to validate the protocol's ability to establish routes and to judge the usefulness of the routing information contained in the routing messages.
The following paper describes how CP-nets were used to model and analyse DYMO. The model utilizes a common net structure, with functions in arc expressions representing routing algorithms. The common CPN pattern can be used to model other on-demand routing protocols for MANETs.
The Generic Access Network (GAN) architecture allows telephone services, such as SMS and voice-calls, to be accessed via generic IP networks. The GAN specification relies on two Internet protocols to provide encryption across IP networks. The detailed usage of these two internet protocols is only roughly sketched in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a more detailed GAN scenario which describes how the two protocols are to be used during the connection establishment procedure. These papers present CPN models developed to formally specify and validate the detailed GAN scenario considered by TietoEnator.
The Session Initiation Protocol (SIP) is a control protocol for initiating, modifying and terminating multimedia sessions over the Internet. SIP uses an INVITE transaction to initiate a session. This paper presents a CPN model for the INVITE transaction. The general properties of the INVITE transaction are verified by analysing the state space of the CPN model. The analysis results show that in most cases the INVITE transaction behaves as expected. However, in some circumstances, the transaction may terminate in an undesirable state. A revised INVITE transaction is proposed and is shown to terminate as expected.
The following papers describe how CP-nets and their supporting computer tools have been applied in the development of communication protocols for interconnecting backbone networks and mobile ad-hoc networks. CPN models and simulation have been used to specify the communication and mobility scenarios to be supported. CPN modelling and state space analysis have been applied to verify the key properties of an edge router discovery protocol to be executed between edge router in a backbone network and gateways in the mobile ad-hoc networks.
The following paper presents the modelling and analysis of a number of variations of the TCP protocol. The work was part of a larger modelling project conducted in cooperation with Hewlett-Packard.
The following papers present a formal model of TCP connection management using CPN. The model is created to verify TCP's functional correctness rather than its performance properties.
The following paper describes how CP-nets and the CPN tools were used to build a formal, executable specification of a standard network protocol, which substituted for a less formal approach using SDL diagrams (augmented by extensive, informal textual descriptions). The project was done in cooperation with a large telecommunications company in the US.
The project is also described in Chapter 9 of:
The paper describes how CP-nets and the CPN tools were used to model and analyse the WAP Class 2 Transaction Service as a first step towards verifying the Wireless Transaction Protocol (WTP). WTP is a protocol layer of WAP and provides a reliable request/response service for Web applications. The state space tool was used to identify some deficiencies in the WTP specification. For instance the specification lacks a description of what constitutes the end of a transaction.
The following paper describes the use of the state space method to verify a revised version of WTP, to gain a high level of confidence in the correctness of the design. Full state space analysis was used to prove properties of the protocol for maximum values of the retransmission counters used in GSM networks (values are 4). However, the size of the state space grows rapidly as the maximum counter values are increased. The sweep-line method was applied in order to take advantage of the progress present in the protocol, notably the progression through major states of the protocol entities, and the increasing nature of the retransmission counters. The sweep-line method allows to prove properties of the protocol for larger counter values than full state space analysis, including those used in Internet Protocol (IP) networks (where the maximum values are 8). As a result, verification of WTP can be performed for the two most important networks, the ones the WAP standard gives recommended maximum values for the retransmission counters.
The following papers describe how CP-nets and the CPN tools were used to model and analyse the ITU-T recommendation H.245, "Control Protocol for Multimedia Communication". Analysis of the model of the Capability Exchange Signalling protocol of H.245 showed that this protocol performs well in general, but some inadequacies also have been found.
The following paper describes how CP-nets Nets and Design/CPN were used for modelling and analysing IOTP, focussing on its protocol architecture. Simulation, message sequence charts, and state space analysis were applied in order to to validate the CPN models of IOTP exchanges and transactions, and to validate that the suggested protocol architecture conforms to the specification of IOTP given in the RFC.
The Internet Open Trading Protocol (IOTP) is an international standard (RFC 2801) currently being developed by the Internet Engineering Task Force. IOTP aims at providing an interoperable framework for electronic commerce (e-commerce) over the Internet. In the following paper CP-nets are used to construct an executable model of the IOTP Deposit Transaction. Due to the formal semantics of CP-nets, this CPN model constitutes an unambiguous specification of the Deposit Transaction and allows us to conduct a formal analysis of the Deposit Transaction. This initial analysis has already revealed minor deficiencies in the Deposit Transaction procedures demonstrating the benefit of applying formal methods for the specification and development of complex communication protocols.
In the following paper a service specification for the Internet Open Trading Protocol (IOTP) is developed using CP-nets. To handle IOTP's complexity, a protocol engineering methodology based is applied on Open Systems Interconnection (OSI) principles consisting of four iterative steps: the definition of service primitives and parameters; the creation of an automaton specifying the local service language for each of the four trading roles of IOTP; the development of a CPN model specifying the global service language for IOTP capturing the correlation between the distributed trading roles; and lastly a new step, language comparison to ensure the consistency between the specifications of the local service language and the global service language. The outcome is a proposed (formal) service specification for IOTP.
The purpose of the following paper is to apply the sweep-line method to a revised IOTP CPN model on order to obtain results for larger parameter values than is possible using conventional analysis and to provide more experience an applying the sweep-line method to practical examples. Another objective is to provide a comparison between the effectiveness of sweep-line analysis when using a progress mapping based on general protocol properties and one based on IOTP-specific properties when analysing the revised IOTP CPN.
The Stream Control Transmission Protocol (SCTP ) is a reliable unicast transport protocol. Its design rationale aims to overcome the weaknesses of the Transmission Control Protocol (TCP). This paper presents a Coloured Petri Net (CPN) model of the revised version of SCTP’s connection management, in particular the revised Tie-Tag mechanisms that differ significantly from the original specification. Preliminary results from state space analysis reveal two potential problems.
E-contracting, i.e., establishing and enacting electronic contracts, has become important. However, the establishment of an e-contract is complicated and error prone. There are multiple negotiation styles ranging from auctions to bilateral bargaining. This paper provides an approach for modeling multi-party negotiation protocols in Coloured Petri nets. It is shown how different negotiation styles can be modeled in a unified and consistent way. Moreover, CPN Tools is used to analyze the resulting Coloured Petri nets. Simulation can be used for both validation and performance analysis, while state-space analysis can be used to discover anomalies in various multi-part negotiation protocols.
The Contract Net Protocol was developed to facilitate contract negotiation in Multi-Agent Systems, between an auctioneer and many bidders. It is therefore important to analyse the protocol to ensure that it terminates correctly and satisfies other important properties. A CPN model of the protocol is presented, and analysis of the model shows that the protocol terminates correctly and that there is no dead code.
In this paper a system based on Controller Area Network is modeled using timed colored Petri nets. This system is verified for the desired properties and then it is validated. Validation is done using two real-life vehicle control units used in light rail applications. The results, as well as possible future use of the model, are presented.
The following paper describes how CP-nets are used to model and analyse mechanisms for resisting Denial-of-Service (DoS) attacks in key exchange protocols. The paper presents models for two cryptographic protocols: one is the well-known Internet protocol named Secure Socket Layer (SSL) protocol, and the other one is the Host Identity Protocol (HIP). Simulation is used to estimate computational costs of protocol execution as well as the percentage of successful connections from legitimate users, under four different strategies of DoS attack.
The following paper describes a CPN model of the SIP-based discovery protocol for the Multi-Channel Service Oriented Architecture (MCSOA). The Multi-Channel Service Oriented Architecture (MCSOA) is an enhanced Service Oriented Architecture (SOA) geared towards the Net-Centric Enterprise Solutions for Interoperability (NESI) initiative of the US Department of Defense (DoD) and Defense Information Systems Agency (DISA). The work presented is part of a larger project to integrate a CPN-based model-driven approach into MCSOA software development.
The following papers describe a number of projects that studied the feasibility of using CP-nets and the CPN tools for the specification of services in intelligent telecommunications networks. The basic idea of the Object-Oriented Petri Net Method (OOPM) is to regard a system as a set of interacting roles (which are parts of objects). First the individual roles and their interactions are identified. Then each role is specified by means of CP-nets and these nets are validated, both individually and as a whole. Finally, the roles are mapped into objects.
One of the projects is also described in Chapter 7 of:
This paper describes how CP-nets and the CPN tools were used to model and analyse a subnetwork reconfiguration protocol for a Metropolitan Area Network. The use of CP-nets replaces a number of commonly used informal specification practices.
The following paper describes how CP-nets and the CPN tools have been used to model the centralised architecture of the timed-token Fieldbus protocol. The performance evaluation dealt with two different policies of asynchronous bandwidth allocations, one being static and the other dynamic.
The following paper describes how CP-nets and the CPN tools were used to model four different ISDN supplementary services. The Integrated Services Digital Network (ISDN) is a fast telecommunications network which customers access via a set of 64 kbps traffic channels. It supports a wide range of basic teleservices, such as telephony, facsimile, and data transmission. To enhance the basic services, a set of supplementary services may be offered.
The project is also described in Chapter 6 of:
The following paper describes how CP-nets and the CPN tools were used to specify, validate, and verify a protocol used by Bang & Olufsen in their audio/video systems.
The project is also described in Chapter 3 of:
The following paper describes how CP-nets and the CPN tools have been used to design and validate the MAC layer of a bus LAN using the CSMA/CD access protocol. The design is based on the IEEE 802.3 standard.
The following papers studies the performance of different Usage Parameter Control (UPC) algorithms for high speed Asynchronous Transfer Mode (ATM) networks. Timed CP-nets and the CPN tools were used to investigate four different UPC algorithms, proposed in the protocol literature. The traffic was generated by a separate CPN model, which simulates Markov Chain Processes.
The project is also described in Chapter 2 of:
The following paper presents a project where CP-nets were used for the detailed design and specification of a software module for the network management system of a European wide area network. The module was designed using the CPN tools, in particular the CPN editor and the CPN simulator. Furthermore, place invariant techniques were used to verify properties of the software module.
The project is also described in Chapter 16 of:
The following paper describes how CP-nets and the CPN tools were used to model MASCOT Pool IDA Communication Mechanisms. It is shown that CP-nets is an effective way for verifying the correctness of the interprocess mechanisms used by parallel architectures of distributed real-time systems.
The following paper describes how CP-nets and the CPN tools were used to model and analyse a new resource reservation internet protocol which is used to convey quality of service information along the path of a data flow. Simulation, message sequence charts, and the state space tool of Design/CPN are used. Although further analysis is needed in order to fully validate the specification, the CPN model provides a well-defined description, which is otherwise seldomly available with Internet protocol engineering activities.
A proposed distributed dynamic channel allocation algorithm was modelled with predicate/transition nets. The Maria reachability analyser was used to analyse the protocol. Among other things, the it was found that the protocol is deadlock-free for some simple configurations.
The paper describes the use of Coloured Petri Nets and Design/CPN in the development of a protocol to support the visualisation and animation of a range of systems that can be modelled using CPNs.
The following paper evaluates the network response time for a switched LAN using CPN. The hardware components are switches, servers, and workstations.
