基于进程代数的多路访问协议模型研究与实现

摘要

通信需要各种协议的参与，如何描述这些协议，如何确保这些协议的一致性，正确性和完备性成为一个难题。人们提出了很多理论来刻画这些协议，如Petri网，形式化方法等。进程代数属于形式化方法的一种，它具有强大的机制，对于分析和描述复杂的网络协议拥有较大的优势。
　　 多路访问协议是为了解决媒体存取控制子层中数据帧发送问题而提出的一簇协议。分析协议内容可知，它所解决的是多个客户端同时向通信信道发送数据的问题，明了的说就是解决的多个进程并发的问题。多个进程在资源有限的情况下，如何利用有限的资源让系统推行下去，是该协议所要解决的问题。
　　 本文的目的在于以多路访问协议为基础，抽象出多进程并发的共同特征，提出一种简单的通用模型，使用进程代数分支之一--通信系统演算(CCS)对模型进行形式化建模。使得该模型不仅适用多路访问协议也能适用于其它多进程并发问题，如多核CPU调度模型中。最后，使用模型检验工具ECW对模型的正确性进行证明，并把该模型应用到多路访问协议和多核CPU调度模型中以检验模型的适用程度。

目录

文摘

英文文摘

声明

第一章 绪论

1.1 本文研究的背景

1.2 相关领域的研究状况

1.3 论文的研究内容及创新之处

1.4 论文的内容安排

第二章 CCS的发展历程

2.1 形式化技术发展回顾

2.1.1 形式化方法起源及发展

2.1.2 形式化方法定义

2.1.3 形式化方法研究内容

2.1.4 形式化方法分类

2.2 进程代数分类

2.3 CCS及其相关技术

2.3.1 CCS的基本计算

2.3.2 CCS基本定律

2.3.3 等价性理论

2.4 CCS模型的验证方式

2.4.1 手工证明

2.4.2 ECW自动化证明

第三章 对多路访问协议的研究

3.1 载波侦听多路访问协议

3.2 CSMA＼CD协议原理

3.3 CSMA＼CD协议控制流程

3.4 多路访问协议本质问题

第四章 利用形式化语义构建通用模型

4.1 构建通用模型

4.1.1 单一进程模型

4.1.2 二进程模型

4.1.3 多进程模型

4.2 通用模型的验证

4.2.1 Hennessy—Milner逻辑

4.2.2 模型验证

第五章 多进程模型的应用

5.1 多进程模型在多路访问协议的应用

5.1.1 多路访问协议系统模型分析

5.1.2 构建多路访问协议系统模型

5.2 多进程模型在多核计算机系统中的应用

5.2.1 多核计算机系统模型

第六章 总结和进一步的工作

6.1 工作总结

6.2 下一步的工作

附录

参考文献

攻读硕士学位期间的研究成果

致谢