论文部分内容阅读
模型检测是协议验证的技术之一。在CSMA／CD协议的验证过程中对该协议进行了简化，忽略了通道时延、退避算法等细节，运用Promela语言进行建模实现。最后，使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环进行了分析和检验，并从结果的有效性和正确性方面得出了相应验证输出图。