论文部分内容阅读
路由协议被广泛部署于因特网中用来进行路由信息的交换与路径的选择，确保路由协议正确、安全的运行是计算机网络的基础问题之一。近年来，形式化验证已成功应用于协助路由协议的设计和实现，形式化方法的使用能够找到软件测试过程中难以发现的系统缺陷，从而有效地提高系统的安全性。主要介绍了自动形式化验证的几类主要技术基础：模型检验、定理证明和等价性验证。总结了自动形式化验证路由协议的方法和优缺点以及它们在各个方面的研究进展和使用状况，为相关方向的研究者在使用形式化方法验证路由协议时提供了参考依据。最后总结了该领域的研究状况