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