论文部分内容阅读
模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例;实验二建立关注节点加入、失效和相应处理的Chord模型,寻找协议缺陷.两个模型都用显式模型检验工具SPIN和有界模型检验工具CBMC实现验证,实验结果表明SPIN解决此类问题更有优势.
Model checking verifies convergence of routing protocols, loop problems, package delivery failures, problems due to ambiguity in protocol descriptions, security flaws, etc. In the first experiment, an OSPF model that focuses on link state database synchronization is set up to set up an attacker router forgery Message to find the counterexample of the successful attack.Experiment 2 establishes a Chord model which focuses on node join, invalidation and corresponding processing, looking for the protocol flaw.The two models are verified by the explicit model test tool SPIN and the bounded model test tool CBMC, and the experimental results This shows that SPIN is more advantageous for solving such problems.