Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
复制标题
DOI：
10.1007/s00165-012-0270-3
复制
发表时间：
2014-05-01
影响因子：
1
通讯作者：
Sevegnani, Michele
中科院分区：
文献类型：
--
作者：
Calder, Muffy;Sevegnani, Michele
随机双图反应系统(SBRS)是最近提出的一种用于模拟在时间和空间上演化的系统的形式化方法。然而，底层空间模型基于树的集合，因此不能以简单或直观的方式表示在几个实体之间共享的空间位置。我们采用了一种扩展的形式，带共享的SBRS，其中的拓扑由有向无环图结构来建模。首先介绍了共享SBRS的概念，然后对其进行了扩展，提出了一种具有指数退避的802.11 CSMA/CARTS/CTS协议模型，该模型适用于信号可能重叠的任意网络拓扑。该模型使用共享来模拟重叠连通区，使用瞬时优先规则进行确定性计算，并使用具有指数反应速率的随机规则来模拟恒定和均匀分布的超时和恒定传输时间。模瞬时反应的模型状态的等价类产生CTMC中的状态，可以使用模型检查器PRISM进行分析。我们在一个具有三个重叠信号的简单示例无线网络上说明了该模型，并给出了一些示例量化性质。
Stochastic bigraphical reactive systems (SBRS) is a recent formalism for modelling systems that evolve in time and space. However, the underlying spatial model is based on sets of trees and thus cannot represent spatial locations that are shared among several entities in a simple or intuitive way. We adopt an extension of the formalism, SBRS with sharing, in which the topology is modelled by a directed acyclic graph structure. We give an overview of SBRS with sharing, we extend it with rule priorities, and then use it to develop a model of the 802.11 CSMA/CA RTS/CTS protocol with exponential backoff, for an arbitrary network topology with possibly overlapping signals. The model uses sharing to model overlapping connectedness areas, instantaneous prioritised rules for deterministic computations, and stochastic rules with exponential reaction rates to model constant and uniformly distributed timeouts and constant transmission times. Equivalence classes of model states modulo instantaneous reactions yield states in a CTMC that can be analysed using the model checker PRISM. We illustrate the model on a simple example wireless network with three overlapping signals and we present some example quantitative properties.