随着网络和通信技术的高速发展,大量新的协议不断被提出.但是,到目前为止,Internet的协议标准RFC仍然使用自然语言描述,Internet的协议实现也主要是采用人工编制完成,这种协议软件开发是随意的,并逐步扩大的.随着网络服务要求的提高,网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性,网络协议再也不可能用工程直觉方法设计出高质量的协议,协议的完整性、正确性、安全性、可移植性和标准化都难以得到保证,而且协议实现后纠正协议描述错误的代价是十分可观的.错误或不完全的协议可能导致整个网络的瘫痪,以及服务可靠性的降低.这就要求我们必须在协议投入实际应用之前,进行协议验证,来保证协议设计的正确性和完整性.也就是说,为了更好地研究和实现协议,应该采用协议工程的方法,通过适当的技术和计算机辅助工具,来设计和维护网络协议.协议形式化理论是协议工程学的核心.形式化验证技术在协议的验证工作中,具有良好的发展前途,并且近几年来受到了广泛的重视.形式化说明语言MSC(消息序列表),在网络协议的设计和文档中越来越受到欢迎.该文给出了使用模型检查技术,对IPv6的邻居发现协议进行形式化验证的方法.我们采用MSC为IPv6的邻居发现协议建立模型,通过线性时序逻辑LTL来描述其安全和活属性,同时,该文中还对解决该协议的形式化验证过程中可能遇到的状态空间问题,提出了一些建议.