Formal Specification and Model-Checking of CSMA/CA Using Finite Precision Timed Automata
Liang Li, Huadóng Ma, Guangyuan Li · 中国邮电高校学报：英文版 · 2005
This paper presents the formal specification and model-checking 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.