Evaluation of a sensor network node communication using formal verification

Sensor networks are low power and low cost embedded system they have limitations like speed and memory. Most sensor networks communicate wirelessly and have variety of applications. One application of sensor networks is discussed in this paper which is to sense temperature remotely. It was observed after computer simulations that the base station was not able to receive temperature data of all nodes i.e. throughput is not 100%. We verified embedded code of sensor networks by implementing it using formal modeling techniques. We modeled multiple concurrent node and an event generator to sense temperature from the environment. Throughput was checked by applying properties using UPAAL model checker. The properties failed indicating why throughput was not 100%. The trace confirmed that the main culprit was the FIFO used in nodes. We then formally modeled FIFO of motes and it was found FIFO overflows in certain cases when data traffic is too high. The FIFO is remodeled by adjusting its size and verified using formal modeling until we were able to satisfy the 100% throughput property. We thus have proved that formal modeling can detect and remove bugs and worst cases which are not evident using computer simulations. This paper discusses this innovative methods of finding bugs in sensor networks by using formal verification and share the results with research community.