Feasibility study of formal analysis of MAC protocols forwireless sensor networks

Abstract: During the last decade the research on sensors have exploded. Starting fromsensors with only few hours of life time until today they have evolved tosmall wireless ones, with many years of life time. Introducing wirelesscommunication capabilities to sensor nodes has added a lot of challenges.Shrinking size of the sensor requires transceivers to be extremely small.Even with small radio devices transmitting data over wireless medium isenergy consuming. To prolong the life time of the sensor many attempts havebeen made to minimize energy usage of transceivers. A successful approach isto duty-cycle transceivers. The radio device is shut down during the periodthat no transmissions are ongoing. However active transceivers that canwake-up on the transmission have not been developed yet. Therefore a lot ofresearch has been focused on the MAC protocol for wireless sensor network,WSN. With an ideal MAC protocol the transceiver should only be on when thereis an ongoing transmission. Nevertheless this is an ideal scenario and due tomedium unreliability, synchronization issues and distributed nature of WSN isnot possible yet. Researchers have developed a lot of MAC protocols and manyof them are mostly applicable for specific scenarios, others are moregeneral. The variety of the MAC protocols poses a challenge for the developerof the applications for WSN. The developers have to analyze the protocols andmake a decision on which one to choose. This is not a simple task because theMAC protocol can be available in pseudo code format, written in C/C++ orother language. The creator of the protocol may have optimized code making ithard to read and most importantly to compare to other MAC protocols. The testscenario may be slightly different from the developers setup. The questionaddressed in this Master Thesis is how do you choose the proper MAC protocol?In this thesis we work on developing a formal method for describing the MACprotocol. Using components we can describe and analyze the MAC protocol in asimple way. We can compare the desired metrics such as delay and energyconsumption of different protocols. The positive side effect is thatcomponents can be reused in different MAC protocols therefore allowing rapiddevelopment of new protocols and optimize existing ones for the specificsituation.