TY - GEN
T1 - Modeling and verification of custom TCP using SDL
AU - Hu, Kai
AU - Cheng, Liu
AU - Kai, Liu
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - SDL
KW - custom TCP
KW - modeling
KW - verification
UR - https://www.scopus.com/pages/publications/84890061212
U2 - 10.1109/ICSESS.2013.6615347
DO - 10.1109/ICSESS.2013.6615347
M3 - 会议稿件
AN - SCOPUS:84890061212
SN - 9781467349970
T3 - Proceedings of the IEEE International Conference on Software Engineering and Service Sciences, ICSESS
SP - 455
EP - 458
BT - ICSESS 2013 - Proceedings of 2013 IEEE 4th International Conference on Software Engineering and Service Science
T2 - 2013 4th IEEE International Conference on Software Engineering and Service Science, ICSESS 2013
Y2 - 23 May 2013 through 25 May 2013
ER -