University of Pernambuco, Recife (BRAZIL)
CADP (Construction and Analysis of Distributed Processes)
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
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.
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.
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
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: http://cadp.inria.fr/case-studies|