Formalized Description and Analysis of FTP on Petri Net

The formal description and analysis of protocol is an important prerequisite for protocol implementation and testing. We can utilize it to reduce the defects in the design of the protocol, to improve the efficiency of protocol development and to promote the development of protocol Standardization. In this paper, firstly we study the working precedure of FTP, and then we used petri net to give a formalized description of FTP concentrating on its control connection and data connection. On the basis of previous work, we analyzed the boundedness, reversibility and liveness of FTP through building up its reachability tree. In that case we can further the analysis of FTP protocol and improve it.