Formal Analysis of Collision Prevention of Two Wireless Personal Area Networks
Amjad Gawanmeh, Youssef Iraqi · Procedia Computer Science · 2016
There are several challenges in the design and operation of Wireless Personal Area Networks (WPANs) such as wireless networking and communication, power consumption, and mobility. Hence, the operation of several WPANs within the same area can result in collision if two WPANs operate in the same wireless channel and come in close range. Therefore, methods for collision detection and prevention need to be validated properly due to the sensitivity of the applications of WPANs. Existing approaches depend on paper and pencil methods to proof the correctness of proposed methods, which might not be enough when practical issues, such as mobility, are taken into consideration. In this paper, we use formal analysis in order to verify the correctness of collision prevention conditions for two WPANs.