A coloured Petri net approach to protocol verification

The correct operation of communication and co-operation protocols, including signalling systems in various networks, is essential for the reliability of the many distributed systems that facilitate our global economy. This paper presents a methodology for the formal specification, analysis and verification of protocols based on the use of Coloured Petri nets and automata theory. The methodology is illustrated using two case studies. The first belongs to the category of data transfer protocols, called Stop-and-Wait Protocols, while the second investigates the connection management part of the Internet's Transmission Control Protocol (TCP). Stop-and-Wait protocols (SWP) incorporate retransmission strategies to recover from data transmission errors that occur on noisy transmission media. Although relatively simple, their basic mechanisms are important for practical protocols such as the data transfer procedures of TCP. The SWP case study is quite detailed. It considers a class of protocols characterized by two parameters: the maximum sequence number (MaxSeqNo) and the maximum number of retransmissions (MaxRetrans). We investigate the operation of the protocol over (lossy) in-sequence (FIFO) channels, and then over (lossy) re-ordering media, such as that provided by the Internet Protocol. Four properties are considered: the bound on the number of messages that can be in the communication channels; whether or not the protocol provides the expected service of alternating sends and receives; (unknowing) loss of messages (i.e. data sent but not received, and not detected as lost by the protocol); and the acceptance of duplicates as new messages. The model is analysed using a combination of hand proofs and automatic techniques. A new result for the bound of the channels (2MaxRetrans+1) is proved for FIFO channels. It is further shown that for re-ordering channels, the channels are unbounded, loss and duplication can occur, and that the SWP does not provide the expected service. We discuss the relevance of these results to the Transmission Control Protocol and indicate the limitations of our approach and the need for further work. The second case study (TCP) illustrates the use of hierarchies to provide a compact and readable CPN model for a complex protocol. We advocate an incremental approach to both modelling and analysis. The importance of stating the assumptions involved is emphasised and we illustrate how they affect the abstractions that can be made to simplify the model. The incremental approach to analysis allows us to validate the model against the TCP definition and to show how errors in the connection establishment procedures can be found. Finally we provide some observations and tips on the how the methodology can be used based on many years of experience. The emphasis of the paper is on providing a tutorial style introduction to the methodology, examining case studies in depth, rather than breadth, and giving some insight into the process while noting its limitations.