局部网络运输协议的形式描述与验证

FORMAL SPECIFICATION AND VERIFICATION OF A TRANSPORT PROTOCOL FOR LOCAL NETWORKS

本文研讨局部网络的运输协议及其形式描述技术.文中论述了局部网络建立运输层的必要性和可能性.讨论了局部网络体系结构中的运输层、运输服务和运输协议的设计,给出了该运输协议的一种基于有限状态自动机(FSA)的形式描述,并通过可达树对该协议的正确性进行了验证.

A transport protocol and its formal description techniques for local networks are discussed. This paper first describes the necessity and the possibility for building the transport layer in a local network. It then presents the transport layer functions, the transport services and a transport protocol design in the local network architecture model: Finally, the transport protocol specification based on the finite state automata (FSA) is given, and the protocol is also verified by using the reachability tree.