ProFuN Research
Our goal is to provide a programming environment where sensors can be programmed as an ensemble rather than individually. Here programmers will focus on the applications and on the services provided by the collection of sensors rather than on which particular sensor to program or on how communication will take place. Energy levels and scheduling will to some extent be controlled by the programmers, e.g., to give priority to specific application tasks. Briefly put, we will employ macro programming of networks of sensors rather than micro programming of individual sensors. We will focus on wireless sensor networks, but the general concept of ensemble programming is applicable to other multiprocessor areas such as grid computing, multicore, and server farms, like Google, etc. We will demonstrate that sensor networks can be programmed as an ensemble under severe constraints, including being devices with very limited capabilities, frequently failing sensors, mobility, energy constraints and harsh security threats.
Programming Support for Macroprogramming
Our goal is to precisely define a small language for macroprogramming, including a formal explanation of its meaning (semantics). This will provide a basis for exporting descriptions in this language to other tools that, e.g., can analyse properties, such as synchronisation or performance, of a network. We have chosen to work with the ATaG (Abstract Task Graph) data-driven programming model, developed by Animesh Pathak (now at INRIA Paris-Rocquencourt, France) together with colleagues (including Amol Bakshi and Luca Mottola) while at UCSC. A compiler and simulator have been implemented. Up to now, the language is explained informally and through examples, which makes it difficult to use the language in other settings, or to apply analysis to ATaG programs. Our effort of formalisation has prompted several suggestions for simplifying the language, so that in effect we are now defining ATaGv2.
Verification
We propose formal models for encoding ad hoc network protocols, and study decidability and undecidability results for the verification of such models. We have recently developed algorithms that can handle protocols with intricate component behaviours and with dynamic network topologies. We concentrate on model checking techniques where the communication topology is represented by a graph and where each node is represented by an automaton communicating with its neighbours via broadcast messages. We consider verification problems formulated in terms of reachability, starting from initial configurations of arbitrary size, of a configuration that contains at least one occurrence of a node in a certain state. One current challenge is to consider networks where both the nodes and the communication between nodes may have timed or stochastic behaviours.
Optimisation
The goal is to model and solve the combinatorial problems identified (by us and others) within the project, for instance in the pre-configuration phase at the middleware level, such as:
- Optimal placement of sensors in the network before deployment.
- Optimal subset and schedule of sensors to be activated after deployment.
- Optimal clustering.
The used constraint solving technologies will be classical constraint programming (by propagation-based systematic search), constraint-based local search, or whatever (possibly hybrid) optimisation/satisfaction technology is more appropriate.
Security
We have improved an algorithm for secure in-network data aggregation in WSNs, making it efficient for use also in smaller networks (from around 30 nodes). The most heavily burdened node sends three times fewer messages than in the scheme before our improvements. We also show how to trade off higher node congestion for decreased total communication load, and have validated our improvements experimentally. Decreasing the communication load and node congestion increases the lifespan of the wireless sensor network by saving considerable battery power.
We are exploring the issues appearing in location-based WSN services, with respect to privacy and anonymity of users. We study existing protocols as well as weaknesses under different attacker scenarios, and provide improved solutions backed by experimental validation.
Semantic Modelling
As a basis for formal modelling and reasoning about WSN programming, we have developed a general framework for process calculi, with expressivity and applicability significantly exceeding earlier work. The framework is very flexible, yet stands on extremely solid theoretical ground. It allows application-specific data and logics, supports compositional reasoning, replacing semantically equivalent modules for each other, and has a machine-checked meta-theory.
We are extending the psi-calculi framework in order to accommodate WSN programming, where we are currently implementing an analysis tool, finalising broadcast/multicast communication primitives, and plan to continue with general resource-aware communication and computation. The strong formal foundation of psi-calculi, with machine-checked meta-theory, together with its intrinsic generality in allowing application-specific data and logics, will provide a flexible yet formal basis for modelling and reasoning about WSN programming.
Testbed
One purpose of a testbed is to be able to download generated code into the nodes, run it in a real environment, and measure the efficiency of the code, language constructs, and underlying middleware. To that purpose, we have completed the UU-Sensei testbed. It is a unique WSN testbed, emphasising repeatable experiments, allowing moving sensors, and providing extensive measurements of communication performance and energy consumption. The testbed is based on a full-fledged computer acting as a host for each sensor. Sensors attach to the host via a local interface, i.e., USB, with a controllable power interface. The hosts themselves communicate via 802.11g/n in an ad hoc fashion to avoid sharing infrastructure with the system under test, while still allowing mobility. The hosts are connected to a control computer for observation and remote configuration of the system.
Middleware
WSN middleware can be seen as the glue between applications, networks, hardware, and operating systems. A complete middleware solution should contain a run-time environment supporting the programming language, multiple applications and mechanisms to achieve adaptive and efficient systems under constrained energy budgets, failing sensors and mobility.
The objective is to define a set of uniform services for the application programmer and to hide the heterogeneity of the system, ensure security, provide quality of service and manage a changing connectivity topology. From the programmer´s point of view these services should either be hidden or provided as a set of APIs and/or libraries.
The run-time system itself may consist of: (i) scalable virtual machines hiding heterogeneity, (ii) publish/subscribe mechanisms of services, and (iii) dynamic code loading and migration of code. We have implemented a pub/subscribe mechanism to detect services and methods to detect communication quality to neighbors.
Demonstrator 1: Indoor Climate Control
We aim at controlling the climate for individuals in buildings while optimising the energy consumption and user comfort. About 40% of all energy generated in the world goes to our buildings. It is dominated by cooling and heating, and the cooling is expected to increase dramatically in growth countries (e.g., "tiger economies") with warm climate.
Sensors will monitor presence, temperature, humidity, luminance, carbon dioxide, drafts, and other physical comfort factors. Individuals may have different preferences, which should also be collected by the system. All this information is forwarded to, and used by, the HVAC system to steer cooling, heating, ventilation, and solar influx with a precision that is not possible today, in order to save energy. Since this requires many different sensors placed with high density to match the individuals using the building, it is expected that there may be as many as one sensor per square meter. It is not feasible to program these sensors individually in a large building; instead it should be done at a higher layer of abstraction.
We will install such a system in our lab and study programming issues on a long-term basis. We will demonstrate the control system in the planned Uppsala Energi house in collaboration with Swedish and international partners in an EU project.
Demonstrator 2: Monitoring and Control of Urban Water Systems
We have built a simulator that combines a model for a wastewater treatment plant (activated sludge model) and a model for a WSN. The simulator gives us a unique environment to benchmark WSNs for monitoring and control in a wastewater treatment plant. We have also started to develop strategies that require lower sampling rates but still give a good control performance. A key idea is to take into account the periodic pattern of the influent disturbances in an iterative learning algorithm.