TY - GEN
T1 - Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking
AU - Zhou, Conghua
AU - Wang, Yong
AU - Cao, Meiling
AU - Shi, Jianqi
AU - Liu, Yang
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/10/26
Y1 - 2015/10/26
N2 - In vehicular ad-hoc network, Media Access Control (MAC) is one of the technologies which determine whether the information is transferred reliably and timely or not. It is also a key to the quality of service of self organization networks. Some behaviors of the MAC protocol can be estimated by experiment and simulation. But the main drawback of these methods is that the estimation can not be accurate to support the enough confidence. In this paper, we complete the precise analysis of the MAC protocol by probabilistic model checking. First, based on the nature of MAC, its dynamic behavior is abstracted into a probabilistic timed automata which can describe non-deterministic, continuous time and the probability selection of MAC. Then we calculate the probability of the data sent successfully and the probability of the backoff counter reaching the maximum value. The analysis result shows that the probability of conflict in 802.11p is much smaller than the 802.11 standard. Therefore the waiting time in 802.11p is significantly reduced and in the case of fast-moving, the data can be sent timely. Further we calculate the maximum expect conflict number under the different values of maximum backoff and the longest time to complete the data transmission. The result shows that when the value of maximum backoff increases, the number of collisions that occurred in 802.11p tends to be stable, which is less than the 802.11 standard's collisions, and the average speed of the data transmission in 802.11p is as four times faster as the 802.11 standard.
AB - In vehicular ad-hoc network, Media Access Control (MAC) is one of the technologies which determine whether the information is transferred reliably and timely or not. It is also a key to the quality of service of self organization networks. Some behaviors of the MAC protocol can be estimated by experiment and simulation. But the main drawback of these methods is that the estimation can not be accurate to support the enough confidence. In this paper, we complete the precise analysis of the MAC protocol by probabilistic model checking. First, based on the nature of MAC, its dynamic behavior is abstracted into a probabilistic timed automata which can describe non-deterministic, continuous time and the probability selection of MAC. Then we calculate the probability of the data sent successfully and the probability of the backoff counter reaching the maximum value. The analysis result shows that the probability of conflict in 802.11p is much smaller than the 802.11 standard. Therefore the waiting time in 802.11p is significantly reduced and in the case of fast-moving, the data can be sent timely. Further we calculate the maximum expect conflict number under the different values of maximum backoff and the longest time to complete the data transmission. The result shows that when the value of maximum backoff increases, the number of collisions that occurred in 802.11p tends to be stable, which is less than the 802.11 standard's collisions, and the average speed of the data transmission in 802.11p is as four times faster as the 802.11 standard.
KW - IEEE 802.11p
KW - media access control
KW - probabilistic model checking
KW - probabilistic timed automata
UR - https://www.scopus.com/pages/publications/84958170183
U2 - 10.1109/TASE.2015.22
DO - 10.1109/TASE.2015.22
M3 - 会议稿件
AN - SCOPUS:84958170183
T3 - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
SP - 55
EP - 62
BT - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
Y2 - 12 September 2015 through 14 September 2015
ER -