%0 Journal Article
%T 使用模型检验自动化验证路由协议
%A 陈哲
%A 马银雪
%A 黄吴丹
%A 黄志球
%J 中山大学学报（自然科学版）
%D 2015
%X 摘要 模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例；实验二建立关注节点加入、失效和相应处理的Chord模型,寻找协议缺陷.两个模型都用显式模型检验工具SPIN和有界模型检验工具CBMC实现验证,实验结果表明SPIN解决此类问题更有优势
%K 模型检验
%K 路由协议验证
%K 形式化方法
%K SPIN
%K CBMC
%U http://xwxt.sict.ac.cn/CN/abstract/abstract3142.shtml