摘要
模型检测是协议验证的技术之一。在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.
出处
《计算机应用》
CSCD
北大核心
2013年第A02期235-237,268,共4页
journal of Computer Applications
关键词
PROMELA
SPIN
协议验证
载波监听多路访问
冲突检测机制
形式化
Promela
SPIN （Simple Promela INtepreter）
protocol validation
Carrier sense Multiple Access with Collision Detection （CSMA/CD）
formalization
