Formal Analysis And Research Of Rudp Protocol

With the continuous development of Internet technology and the thriving growth of network users, the user requirements and network applications are diversified. The existing data transmission mode cannot meet the need for higher performance and reliability of communication in some large and complex system applications, which makes concerningstudies imminent. TCP is the current connection-oriented method for reliable data transmission which is characterized by reliability and safety. However, it is based on the transmission of the byte stream, belonging to unboundary protocol with complex processing, low efficiency and high resource costs; it cannot support massive concurrent connections. On the contratry, as a no connection oriented datagram protocol, UDP is fast, highly effiencient, and able to support massive concurrent connections. But it does not have its own flow control and reliable measures, which leads to shortcomings such as poor reliability and limited transmission function.RUDP has emerged as a reliable user datagram protocol in recent years to achieve better data transmission. RUDP a simple packet transmission protocol based on reliable data protocol RDP, which combines the advantages of TCP and UDP.Taking full advantage of UDP’s fast and highly efficient transmission RUDP fully guarantees the reliability of transmission. As for the research of RUDP, there is still a long way to go with limited literature, research methods and formal modelling methods. Within the development of network protocol, formal research method is one of the core technologies for the design and analysis of network protocols. Formal modeling and verification of network protocols have become the basis of the design and implementation of the entire agreement. The formal specification of network protocols can be achieved through formal modeling to lay the foundation for formal description and verification of protocols, comprehensive protocols, protocols testing and protocol validation.Against this backdrop, the paper proposes the formal analysis and research for RUDP protocol. The formal methods include:finite state machines, Petri nets, temporal logic, communication process calculus and Z language. In this paper, finite state machine, Z language and colored Petri nets are selected as formal modeling techniques to model RUDP protocol. Reachability tree, Z/EVES and CPN Tools are employed to analyse and verify those formal models. Those models are contrasted to illustrate the advantages and disadvantages of these three modelling techniques to provide a formal approach to investigate into RUDP protocol.