路由协议的自动形式化验证方法研究  

Research on Automated Formal Verification of Routing Protocols

作　　者：黄吴丹 严俊琦 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机技术与发展》2017年第12期1-6,共6页Computer Technology and Development

基　　金：国家自然科学基金资助项目(61100034);国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130);教育部留学回国人员科研启动基金(2013);中央高校基本科研业务费专项资金(NS2016092)

摘　　要：路由协议被广泛部署于因特网中用来进行路由信息的交换与路径的选择,确保路由协议正确、安全的运行是计算机网络的基础问题之一。近年来,形式化验证已成功应用于协助路由协议的设计和实现,形式化方法的使用能够找到软件测试过程中难以发现的系统缺陷,从而有效地提高系统的安全性。主要介绍了自动形式化验证的几类主要技术基础:模型检验、定理证明和等价性验证。总结了自动形式化验证路由协议的方法和优缺点以及它们在各个方面的研究进展和使用状况,为相关方向的研究者在使用形式化方法验证路由协议时提供了参考依据。最后总结了该领域的研究状况,并对未来研究热点进行了预测和展望,提出了一些可行的研究方向。Routing protocols are widely deployed in the Interoet for exchanging routing information and selecting routes. Having a correct and secure routing protocol is a fundamental problem to computer networks. Recently, formal verification has been successfully applied to ensure quality of routing protocols in design and implementation. And it can effectively find system defects in software testing to enhance the security of systems. The several main techniques in automated formal verification like model checking, theorem proving and equiva- lence verification are introduced primarily. Then the important methods on automated formal verification for routing protocols and their advantages and disadvantages, as well as their research progress and utilization are summarized, which provides a reference for researchers in related fields to verify routing protocols with formal methods. Finally ,the research status of this field is summarized and the future re- search hotspots are forecasted. Some feasible research directions are also put forward.

关 键 词：路由协议 形式化验证 模型检验 定理证明 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]