IEEE 802.15.4 TSCH MAC操作模式簇树形成协议实现的建模与验证
网络与互联网体系结构
2017-03-21 v1 软件工程
摘要
面对自组织无线网络中存在的许多不确定性，无线传感器网络的正确且高效初始化可能具有挑战性。本文中，我们研究了一个在IEEE 802.15.4标准的TSCH MAC操作模式之上运行的网络中形成簇树拓扑的实现，并使用形式化方法对其进行了探究。我们展示了mCRL2语言和工具集如何帮助我们识别该实现未形成适当拓扑的场景。更重要的是，我们的分析得出结论：簇树形成算法具有超线性时间复杂度。因此，它无法扩展到大型网络。
引用
@article{arxiv.1703.06572,
title = {Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode},
author = {Mahmoud Talebi and Jan Friso Groote and Conrad Dandelski},
journal= {arXiv preprint arXiv:1703.06572},
year = {2017}
}
备注
In Proceedings MARS 2017, arXiv:1703.05812