基于概率时间自动机的IEEE 802.15.4非信标网络介质访问控制建模

摘要

本文研究了PRISM概率模型检查器支持的概率时间自动机的非信标IEEE 802.15.4无线局域网中介质访问控制的形式化建模。在这些网络中，设备通过执行无槽载波侦听多址访问和冲突避免算法来竞争媒体。在文献中，介绍了一个由两个站组成的网络模型，该模型向两个不同的目的站发送数据。我们改进了这个模型，并在此基础上提出了两种建模网络的方法，其中任意数量的发送站都有自己的目的地。我们证明了同样的模型是具有任意数量站点的星形网络的有效表示，这些站点向同一目的站点发送数据。我们还提出，如果一些发送站不在其他发送站的无线电范围内，即如果它们被隐藏，如何对这样的网络进行建模。我们给出了利用PRISM对这些模型进行概率模型检验得到的一些结果。

移动信息系统

摘要

版权

更多相关文章