UPPAAL中AODV的建模与分析
网络与互联网体系结构
2015-12-24 v1 计算机科学中的逻辑
摘要
本文描述了针对无线自组网按需距离矢量(AODV)路由协议（一种广泛用于自组织无线网络的协议）进行自动化形式化严格分析的工作进展。我们简要概述了在UPPAAL模型检测器中实现的AODV模型，并描述了为探索AODV在两种网络拓扑中的行为而进行的实验。我们能够自动定位并确认一些已知的异常和不良行为。我们认为这种将模型检测作为诊断工具的使用，补充了其他基于形式化方法的协议建模与验证技术，例如进程代数。模型检测尤其有助于发现协议局限性以及开发改进版本。
引用
@article{arxiv.1512.07312,
title = {Modelling and Analysis of AODV in UPPAAL},
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:1512.07312},
year = {2015}
}
备注
in Proc. 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011