• adaptation layer
• middleware
• post-deployment reconfiguration
• ubiquitous systems
• WSNs

We present a software solution for energy-aware reconfiguration of WSNs. An hybrid approach is proposed for reprogramming sensor nodes, that
combines the efficiency of execution of native code with the flexibility and ease of programming of virtual machines. The main idea is to adapt the behaviour of the application by intercepting system calls to primitives and library functions
made by the application, and modify the effect of such calls by executing specific fragments of code, called adaptlets, to customise the application behaviour. This is achieved by the intervention of an adaptation layer that is seamlessly inserted at the interface between the application and the operating system. The adaptation layer is distinct from the application, and embeds a tiny virtual machine that executes adaptlets meant for post-deployment configuration of the application. Differently from other approaches, where the entire application is interpreted, adaptlets are tied only to specific
services, while the bulk of the application is still written in native code. This makes the proposed approach able to preserve the compactness
and efficiency of native code and to have little impact on the overall application performance. The adaptation layer has been implemented in the context of the TinyOS operating system, and the
instruction set is inspired to the Java bytecode. Examples illustrating the programming of the adaptation layer are presented together with their experimental validation.

Furthermore, in order to support battery-aware operations, we developed B-MAC+, an enhancement of B-MAC, a popular contention-based protocol for WSNs. In particular, we make clear how receivers running the standard B-MAC protocol waste energy during the reception of long preambles and we propose a more efficient solution. Also, we explore the possibility of adopting opportunistic computing paradigms to overcome the problem of executing applications when the size of the program is larger than the amount of memory available on a single node. We propose a technique based on the idea of dividing the application into smaller and cooperating code fragments. Each fragment of the application fits the resources available on a single node, and an opportunistic cooperation between nodes -- either on the path to the base station or within a given region -- can be used to resemble the global computation. FInally, we report on our work towards developing a simulation and analysis framework for WSN algorithms within a theorem prover. Specifically, we explored the possibility of using the evaluation mechanism of the Prototype Verification System (PVS) to specify, test and verify WSN communication protocols during the very early stages of their design. The specification of the algorithm is expressed with an extensible set of programming primitives, and properties of interest are evaluated with ad hoc network simulators automatically generated from the formal specification.