这篇论文论述正式说明并且有用我们为即时系统开发了的模型检查器的碰撞回避(CSMA/CA ) 协议的 CarrierSense 多重存取检查模型,当有限精确的网络预定了自动机,它被指定。CSMA/CA 协议在 IEEE 建议 802.11 标准被设计在无线随机的存取环境在传播期间减少碰撞的概率。然而,它不完全消除在二之间的碰撞或同时播送的更多的框架的可能性。我们调查什么将产生在框架之间的碰撞并且使用我们的自动确认工具为检查模型。
This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance( CSMA/CA) protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.