Database of Case Studies Achieved Using CADP

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:
or from the CADP Web site in PDF or PostScript

Nelson Souto Rosa
Centro de Informatica
Universidade Federal de Pernambuco
50732-970 Recife, Pernambuco

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:03 2021.

Back to the CADP case studies page