Abstract: When specifying and designing computer network protocols, it is convenient to use an abstract synchronous communication mechanism. In practice, however, asynchronous communication mechanisms cannot be avoided. This paper presents a formal approach, based on Hoare's Communicating Sequential Processes (CSP) and some theoretical results, to the specification and design of protocols which ensure the correctness of the protocols regardless of the communication mechanism used in implementation. The Alternating Bit (AB) protocol is used to illustrate our results.

Key words: CSP, computer networks, protocol, communication, formal specification

摘要： 描述和设计计算机网络通信协议时，使用抽象的同步通信机制最为方便。但在实际中，使用异步通信机制将不可避免。基于霍尔的“通信顺序进程”和其他对通信协议描述与设计的理论研究结果，本文提出一个形式化方法，这个方法在不论使用何种实现通信机制的情况下都将保证通信协议的正确性。

关键词: 通信顺序进程, 计算机网络, 协议, 通信, 形式化描述