无线自组织网络的建模与高效验证
网络与互联网体系结构
2017-04-18 v2 计算机科学中的逻辑
摘要
无线自组织网络，特别是移动自组织网络(MANETs)，发展非常迅速，因为它们使通信更便捷、更普及。然而，由于其协议往往难以设计，这归因于无线通信依赖拓扑的行为，以及针对拓扑动态性的分布式与自适应操作。因此，期望使用形式化方法对它们进行建模与验证。本文提出一种基于actor的建模语言，旨在对MANETs建模。我们解决无线自组织网络建模的主要挑战，如本地广播、底层拓扑及其变化，并讨论如何在语义层面高效建模以使验证可行。新框架通过提供异步(本地)广播和单播通信来抽象数据链路层服务，而消息传递有序且对连接的接收者保证送达。我们通过两种路由协议即泛洪(flooding)和AODVv2-11来说明框架的适用性，并展示所提技术如何高效缩减其状态空间。此外，我们展示了通过我们的分析工具在AODV中发现的一个环形成场景。
引用
@article{arxiv.1604.07179,
title = {Modeling and Efficient Verification of Wireless Ad hoc Networks},
author = {Behnaz Yousefi and Fatemeh Ghassemi and Ramtin Khosravi},
journal= {arXiv preprint arXiv:1604.07179},
year = {2017}
}