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 module in LOTOS
© Copyright Policy
Related In: Results  -  Collection

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

f2-sensors-07-01447: nesC module in LOTOS

Mentions: A module is a first-class element of nesC language and has of two basic parts: the set of interfaces provided and used by the module; and the implementation. The interfaces are modelled as defined in Section 3.1. Meanwhile, as the basic abstraction in LOTOS is a process, the nesC module is specified as a LOTOS process (see Figure 2). The implementation of each function (command or event) is defined in the behaviour part of the process using the LOTOS choice operator ([ ]): each command/event defines an option in the choice.


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

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

f2-sensors-07-01447: nesC module in LOTOS
Mentions: A module is a first-class element of nesC language and has of two basic parts: the set of interfaces provided and used by the module; and the implementation. The interfaces are modelled as defined in Section 3.1. Meanwhile, as the basic abstraction in LOTOS is a process, the nesC module is specified as a LOTOS process (see Figure 2). The implementation of each function (command or event) is defined in the behaviour part of the process using the LOTOS choice operator ([ ]): each command/event defines an option in the choice.

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.