Modeling and verification of custom TCP using SDL

With the development of computer network, the complexity of network protocol increases gradually, leading to the difficulty, long cycle, multi-error for protocol development. The protocol engineering works well to solve these problems, which uses formal methods to develop protocols. Although the Transmission Control Protocol (TCP) is widely used as a mature transport protocol, some issues have to be considered when it is achieved in a particular environment, for example, security and logical correctness. In this paper, we modeled for TCP, simulated and verified the model based on the thoughts of protocol engineering. Firstly, we customized TCP according to the specific needs. Then we modeled for TCP using the Specification and Description Language (SDL) which is a commonly used formal description language by the tool SDL Suite. At last we simulated and verified the SDL model. The results showed that the ambiguous terms and some errors for the SDL model could be found. It is helpful for the further development.