Using LOTOS for Formalizing Wireless Sensor Network Applications

The number of wireless sensor network (WSN) applications is rapidly increasing and becoming an integral part of sensor nodes. These applications have been widely developed on TinyOS operating system using the nesC programming language. However, due to the tight integration to physical world, limited node power and resources (CPU and memory) and complexity of combining components into an application, to build such applications is not a trivial task. In this context, we present an approach for treating with this complexity adopting a formal description technique, namely LOTOS, for formalising the WSN applications ‘behaviour. The formalisation has three main benefits: better understanding on how the application actually works, checking of desired properties of the application's behaviour, and simulation facilities. In order to illustrate the proposed approach, we apply it to two nesC traditional applications, namely BLink and Sense.