Modelling Attacker with Deciding Security Properties by Induction and Deduction

Wireless Sensor Networks are becoming one of the most successful choices for the development and deployment of applications in a range of scenarios, from intelligent homes to environment monitoring. Nowadays, there is a growing demand for programming large-scale wireless sensor networks. New programming paradigms should ease the task of building WSN applications that adapt at run-time to changes in the context, in the available resources, and also in user requirements. In this paper we describe PROTEUS, a platform to manage adaptation and reconfiguration, with the aim of supporting the development of WSN applications. After introducing PROTEUS, we show how it can be used to program a dynamic clustering algorithm, where clusters are created and destroyed at runtime, and nodes need to adapt and reconfigure accordingly. We provide a prototype implementation using TinyOS. Some remarks on the work are also presented.