CSMA/CD协议的形式化描述与验证  

Formal description and validation of CSMA/CD

作　　者：张涛[1] 袁键[1] 田宏林[1] 

机构地区：[1]73610部队,南京210018

出　　处：《计算机应用》2013年第A02期235-237,268,共4页journal of Computer Applications

摘　　要：模型检测是协议验证的技术之一。在CSMA/CD协议的验证过程中对该协议进行了简化,忽略了通道时延、退避算法等细节,运用Promela语言进行建模实现。最后,使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环进行了分析和检验,并从结果的有效性和正确性方面得出了相应验证输出图。Model checking is one of the technologies of protocol validation. In the process of validation, a CSMA/CD （ Carrier sense Multiple Access with Collision Detection） protocol was simplified by ignoring channel delay, backoff and so on. And then it was realized and simulated with Premela language. And further more, making use of model checking tool SPIN, this paper gives the analyses and validation results of the correctness, states and cycles of the protocol, and the corresponding verification output charts of the correct and effective results were obtained.

关 键 词：PROMELA SPIN 协议验证 载波监听多路访问 冲突检测机制 形式化 

分 类 号：TP393.04[自动化与计算机技术—计算机应用技术]