Limits...
Using LOTOS for Formalizing Wireless Sensor Network Applications

View Article: PubMed Central

ABSTRACT

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.

No MeSH data available.


nesC Sense application
© Copyright Policy
Related In: Results  -  Collection

License
getmorefigures.php?uid=PMC3814862&req=5

f4-sensors-07-01447: nesC Sense application

Mentions: Similarly to the BLink, the steps defined in Section 3 have also been followed in the specification of Sense application. Hence, the modules and configurations that compose the Sense application were initially identified (see Figure 4): module Main (line 16), module SenseM (line 18), module LedsC (line 21), configuration TimerC (the same as in the Blink application), and configuration Photo (line 25). The configuration Photo only includes a module, namely PhotoTemp, which is a configuration. PhotoTemp is composed by the module PhotoTempM and the configuration ADCC. Finally, the configuration ADCC is made up of modules ADCCM and HPLADCC.


Using LOTOS for Formalizing Wireless Sensor Network Applications
nesC Sense application
© Copyright Policy
Related In: Results  -  Collection

License
Show All Figures
getmorefigures.php?uid=PMC3814862&req=5

f4-sensors-07-01447: nesC Sense application
Mentions: Similarly to the BLink, the steps defined in Section 3 have also been followed in the specification of Sense application. Hence, the modules and configurations that compose the Sense application were initially identified (see Figure 4): module Main (line 16), module SenseM (line 18), module LedsC (line 21), configuration TimerC (the same as in the Blink application), and configuration Photo (line 25). The configuration Photo only includes a module, namely PhotoTemp, which is a configuration. PhotoTemp is composed by the module PhotoTempM and the configuration ADCC. Finally, the configuration ADCC is made up of modules ADCCM and HPLADCC.

View Article: PubMed Central

ABSTRACT

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.

No MeSH data available.