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 spec...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.展开更多
基金The workreportedinthis paperissupported bythe National Grand Fundamental Research973 Programof China (2002cb312200) ,andthe National Nat-ural Science Foundation of China(60242002 ,60273025)
文摘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.
