AODV及其变体的严格分析
网络与互联网体系结构
2015-12-31 v1 计算机科学中的逻辑
摘要
本文使用 AWN (Algebra for Wireless Networks，无线网络的代数) 中的形式化规范，对 Ad hoc On-Demand Distance Vector (AODV) 路由协议进行了严格分析；AWN 是一种专门为建模移动自组织网络与无线网状网协议而量身定制的进程代数。我们的形式化模型刻画了 AODV 核心功能的精确细节，例如路由发现、路由维护和错误处理。我们通过给出环自由性的详细证明，展示了如何利用 AWN 推理关键的协议正确性属性。与基于仿真或模型检测等其他形式化方法的评估不同，我们的证明是通用的，适用于任何可能的网络场景（如网络拓扑、节点移动性、流量模式等）。本文的一个关键贡献是展示了相关推理与证明如何相对容易地适配到协议变体。
引用
@article{arxiv.1512.08873,
title = {A Rigorous Analysis of AODV and its Variants},
author = {Peter Höfner and Rob van Glabbeek and Wee Lum Tan and Marius Portmann and Annabelle McIver and Ansgar Fehnker},
journal= {arXiv preprint arXiv:1512.08873},
year = {2015}
}
备注
arXiv admin note: substantial text overlap with arXiv:1312.7645