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

北京大学学报（自然科学版）

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

孙踊¹, 杨宏戟²

¹贝尔法斯特女皇大学计算机系，贝尔法斯特市，英国; ²蒂蒙特福特大学计算机系，莱斯特市，英国

收稿日期:1996-04-03 出版日期:1997-01-20 发布日期:1997-01-20

Protocol Specification Based on CSP

SUN Yong¹, YANG Hongji²

¹Department of Computer Science The Queen's University, of Belfast BT7 1NN, Northern Ireland, E-mail: Y.Sun@qub.ac.uk; ²Department of Computer Science of De Montfort University, Leicester LE1 9BH, England, E-mail: hiy@dmu.ac.uk

Received:1996-04-03 Online:1997-01-20 Published:1997-01-20

摘要/Abstract

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

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

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

中图分类号:

TP301
TP393

孙踊, 杨宏戟. 基于通信顺序进程的计算机网络通信协议形式化描述[J]. 北京大学学报（自然科学版）.

SUN Yong,YANG Hongji. Protocol Specification Based on CSP[J]. Acta Scientiarum Naturalium Universitatis Pekinensis.

导出引用管理器 EndNote|Ris|BibTeX

链接本文: https://xbna.pku.edu.cn/CN/

https://xbna.pku.edu.cn/CN/Y1997/V33/I1/110

[1]	杨洪章, 杨雅辉, 孙广宇. 基于用户态文件系统的共享访问与性能提升研究[J]. 北京大学学报自然科学版, 2020, 56(6): 1020-1030.
[2]	张竟枢, 吕梦菲, 李斗, 杨延军, 赵玉萍. 一种基于ICA方法的网格化无线电监测方案[J]. 北京大学学报（自然科学版）, 2018, 54(2): 307-314.
[3]	余怀瑾, 依那, 蒋伟, 杨峰. 基于UKF算法的高机动机载平台多普勒频移估计[J]. 北京大学学报自然科学版, 2017, 53(6): 1003-1010.
[4]	张瑞洁, 田原, 刘思叶, 王雯夫. 即时通信文本中地理信息提取——以微信为例[J]. 北京大学学报（自然科学版）, 2016, 52(6): 985-989.
[5]	温淼文,李彦丽,段晓辉,焦秉立. 自适应窄波束在短波对跖通信中的应用[J]. 北京大学学报（自然科学版）, 2011, 47(4): 581-586.
[6]	程正杰,陈克非,来学嘉. 基于细粒度新鲜性的密码协议分析[J]. 北京大学学报（自然科学版）, 2010, 46(5): 763-770.
[7]	凤旺森,陈萍,张蓓. 一种P2P层叠网维护协议的稳定性分析[J]. 北京大学学报（自然科学版）, 2009, 45(4): 589-593.
[8]	汪浩,李晓明,严伟. 一个具有阻行机制的成批到达排队系统GI^X/M/1/N[J]. 北京大学学报（自然科学版）, 2006, 42(3): 406-411.
[9]	韩心慧,司端锋,邹维. 一种基于丢包依赖体现的E模型的自适应播放延迟算法[J]. 北京大学学报（自然科学版）, 2006, 42(3): 388-394.
[10]	丘维声,蔡凯. 周期拟完美序列的构造和计数与循环Hadamard(Ⅱ)型差集的乘子群[J]. 北京大学学报（自然科学版）, 2005, 41(1): 27-35.
[11]	胡璇, 栾胜基. 从环境协议收费现象看排污收费政策的缺陷[J]. 北京大学学报（自然科学版）, 2004, 40(2): 303-309.
[12]	李景聪, 李正斌, 吴德明, 徐安士. IP波长路由器的设计研究[J]. 北京大学学报（自然科学版）, 2003, 39(1): 98-104.
[13]	吴德明, 徐安士, 朱立新, 王子宇, 张肇仪, 谢麟振. 波分复用和频分复用光纤通信技术研究[J]. 北京大学学报（自然科学版）, 1998, 34(2): 214-220.
[14]	张侃, 徐安士, 吴德明, 谢麟振. 波长路由波分复用环形网阻塞特性研究[J]. 北京大学学报（自然科学版）, 1997, 33(5): 621-626.
[15]	顾金星,徐承和. 掺铒氟光纤放大器的理论分析[J]. 北京大学学报（自然科学版）, 1995, 31(5): 599-608.