用于建模、验证和分析 AODV 的无线 Mesh 网络进程代数
网络与互联网体系结构
2013-12-31 v1 计算机科学中的逻辑
摘要
我们提出了 AWN (Algebra for Wireless Networks)，这是一种专为移动自组网 (MANET) 和无线 Mesh 网络 (WMN) 协议建模量身定制的进程代数。它结合了对本地广播、条件单播和数据结构的新颖处理。在此框架下，我们对按需距离矢量自组网路由协议 (AODV) 进行了严格分析；AODV 是一种为 MANET 和 WMN 设计的流行路由协议，也是目前由 IETF MANET 工作组标准化的四种协议之一。我们给出了该协议完整且无歧义的规范，从而将 AODV 的 RFC（事实上的标准规范，以英语散文形式给出）形式化。在此过程中，我们必须做出非显而易见的假设以解决该规范中出现的歧义。我们的形式化模型涵盖了 AODV 核心功能的确切细节，如路由维护和错误处理，仅省略了时序方面。该进程代数使我们能够形式化并证明（或证伪）Mesh 网络路由协议的关键属性，如无环性和数据包交付。我们是首个提供 AODV 无环性详细证明的研究者。与使用仿真或模型检查的评估相比，我们的证明是通用的，适用于任何可能的网络场景（就网络拓扑、节点移动性等而言）。由于 RFC 规范存在歧义和矛盾，它允许多种解释；我们展示了超过 5000 种解释中哪些是无环的，从而证明了推理和证明可以相对容易地适应协议变体。利用我们形式化且无歧义的规范，我们发现了影响 AODV 性能的缺陷，例如建立非最优路由以及完全无法找到某些路由。我们在同一进程代数中形式化了改进措施；沿用这些证明再次变得容易。
引用
@article{arxiv.1312.7645,
title = {A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV},
author = {Ansgar Fehnker and Rob van Glabbeek and Peter Höfner and Annabelle McIver and Marius Portmann and Wee Lum Tan},
journal= {arXiv preprint arXiv:1312.7645},
year = {2013}
}