Analysis of Wireless Sensor Network Applications for TinyOS

Organisation:	University of Pernambuco, Recife (BRAZIL)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2007
Size:	n/a
Description:	WSN (Wireless Sensor Network) applications are spreading out in many areas, including environment, habitat, disaster monitoring, health-care applications, home automation, and traffic control. Such applications are often developed using the TinyOS operating system using the nesC programming language. For the authors, LOTOS was a natural choice to formalize WSN applications since it is an international standard for describing concurrent systems, the hierarchical structure of LOTOS descriptions is similar to the architecture of WSN applications, and the expressiveness of LOTOS allowed the specification at different abstraction levels accommodating the complexity of nesC applications. The authors suggest a four step approach for the representation of a TinyOS application in LOTOS. First, the components (i.e., modules and configurations of nesC) to be represented as LOTOS processes are identified. Second, the connections of theses components define the LOTOS gates and the parallel composition operators. Third, the interface operations are represented as LOTOS data types. Last, the ordering of interactions as defined by the nesC implementation of a module is translated into the definitions of the corresponding LOTOS process. The approach is illustrated on two TinyOS applications taken from the TinyOS distribution: Blink (which toggles a red led on every clock interrupt) and Sense (which periodically samples the photo sensor). Both applications were translated manually into LOTOS. Using CADP, the LOTOS specifications were simulated and checked for absence of deadlocks and livelocks. This allowed to confirm automatically a deadlock in the Blink application.
Conclusions:	LOTOS is an appropriate formalism to describe nesC applications for TinyOS. Using CADP, it was possible to exhibit automatically a deadlock in the Blink application of the TinyOS distribution.
Publications:	[Rosa-Cunha-07] Nelson Souto Rosa and Paulo Roberto Freire Cunha. "Using LOTOS for Formalising Wireless Sensor Network Applications". Sensors 7(8), pp. 1447-1461, August 2007. Available on-line at: http://www.mdpi.org/sensors/papers/s7081447.pdf or from the CADP Web site in PDF or PostScript
Contact:	Nelson Souto Rosa Centro de Informatica Universidade Federal de Pernambuco 50732-970 Recife, Pernambuco BRAZIL Email: nsr@cin.ufpe.br
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page