Feasibility study of formal analysis of MAC protocols for
wireless sensor networks

Abstract: During the last decade the research on sensors have exploded. Starting from
sensors with only few hours of life time until today they have evolved to
small wireless ones, with many years of life time. Introducing wireless
communication 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 is
energy consuming. To prolong the life time of the sensor many attempts have
been made to minimize energy usage of transceivers. A successful approach is
to duty-cycle transceivers. The radio device is shut down during the period
that no transmissions are ongoing. However active transceivers that can
wake-up on the transmission have not been developed yet. Therefore a lot of
research has been focused on the MAC protocol for wireless sensor network,
WSN. With an ideal MAC protocol the transceiver should only be on when there
is an ongoing transmission. Nevertheless this is an ideal scenario and due to
medium unreliability, synchronization issues and distributed nature of WSN is
not possible yet. Researchers have developed a lot of MAC protocols and many
of them are mostly applicable for specific scenarios, others are more
general. The variety of the MAC protocols poses a challenge for the developer
of the applications for WSN. The developers have to analyze the protocols and
make a decision on which one to choose. This is not a simple task because the
MAC protocol can be available in pseudo code format, written in C/C++ or
other language. The creator of the protocol may have optimized code making it
hard to read and most importantly to compare to other MAC protocols. The test
scenario may be slightly different from the developers setup. The question
addressed 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 MAC
protocol. Using components we can describe and analyze the MAC protocol in a
simple way. We can compare the desired metrics such as delay and energy
consumption of different protocols. The positive side effect is that
components can be reused in different MAC protocols therefore allowing rapid
development of new protocols and optimize existing ones for the specific
situation.