基于通信顺序进程的计算机网络通信协议形式化描述

Protocol Specification Based on CSP

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

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.