Parametric protocol verification is a challenging r-e- search topic. Obtaining symbolic representations of service and protocol languages of a protocol enables parametric verification of the protocol against its service specification. In this paper, we exploit recurrent structural regularities of state spaces to obtain symbolic representations of protocol languages for the revised Capability Exchange Signalling (CES) protocol. This leads to conjectures on a recursive expression for the revised CES protocol language and for the inclusion of the revised CES protocol language in the CES service language, for any values of the parameters. This result also demonstrates the promising future of our approach to finding symbolic representations for service and/or protocol languages.

This paper investigates the connection establishment procedures of the Datagram Congestion Control Protocol (DCCP) when sequence numbers wrap. A formal executable specification of DCCP connection management is obtained using Coloured Petri Nets. The model includes the synchronization procedure, sequence number wrapping and the algorithm for extending short sequence numbers. We discover that during connection establishment if sequence numbers wrap, it is possible that the attempt to set up the connection fails.

The capability exchange signalling (CES) protocol is a subprotocol of ITU-T recommendation H.245, "control protocol for multimedia communication". We are interested in verifying this protocol, including verification of its general properties such as absence of deadlocks and livelocks, and verification of the protocol against its service. In previous work, we have analysed the general properties of the CES protocol. In order to verify the protocol against its service, we need to generate the CES service language, which defines all the possible sequences of user observable events. We firstly create the CES service CPN model and then extract the language from the occurrence graph (OG) of the model. In the case of the CES service, this is challenging because we wish to have a general result for arbitrary capacity of the network over which the CES protocol operates. To tackle this problem we introduced into the CPN model a parameter, l, representing the capacity of the communication channel. We derived a recursive formula for the parameterised OG in terms of l. We treat this OG as a finite state automaton (FSA) by nominating acceptance states and apply FSA reduction algorithms to obtain a deterministic FSA that represents the CES service language. We have discovered a recursive formula in l for the CES service language. This paper introduces the CES service via its CPN model as necessary background and presents the final step of the proof of this finding.

State-space exploration is one of the main approaches to computer-aided verification and analysis of finite-state systems. It is used to reason about a wide range of properties during the design phase of a system, including system deadlocks. Unfortunately, state-space exploration needs to handle huge state spaces for most practical systems. Several state-space reduction methods have been developed to tackle this problem. In this paper, we develop algorithms for combining two of these methods: state equivalence class reduction and the sweep-line. The algorithms allow deadlocks to be detected by recording terminal states of the system on-the-fly during state-space exploration. We derive expressions for the complexity of the algorithms and demonstrate their usefulness with an industrial case study. Our results show that the combined method achieves at least a six-fold reduction of the state space for interesting parameter values compared with either method used in isolation while still proving the desired system property of the terminal states. The runtime performance of the combined method is almost the same as that of the equivalence class method over the chosen parameter range. Moreover, the improvement in space reduction increases with increased parameter values.

The PROTEAN protocol emulation and analysis computer aid is presented. It is based on a formal specification technique called numerical Petri nets (NPNs), and provides both graphical (color) and textual interfaces to the protocol designer. NPN specifications may be created, stored, appended to other NPNs, structured, edited, listed, displayed, and analyzed. Interactive simulation, exhaustive reachability analysis, and several directed graph analysis facilities are described. Specification languages are compared, with concentration on extended finite state machines and high-level Petri nets. Both the NPN and PROTEAN facilities are described and illustrated with a simple example. The application of PROTEAN to complex examples is mentioned briefly. Work towards a comprehensive protocol engineering workstation is also discussed.>