I am interested in modeling and analyzing wireless sensor networks. Wireless sensor networks (WSNs) are composed of distributed autonomous nodes, containing programs and sensors to monitor physical or environmental conditions. Each node is a small physical device embedding sensors, a small CPU, a battery, a wireless transceiver and an antenna for communication. WSNs are useful in many contexts, such as environment or health monitoring.
However,the design of WSNs is complex and error-prone due to their numerous constraints:
It is a crucial preoccupation (even more important than quality of service). Overall lifetime of the WSN usually depends on sensor nodes lifetime because nodes have limited battery power.
They lead to important issues such as interleaving of actions and race conditions.
WSNs may contain various types of nodes, each having different characteristics (embedded sensors, wireless range, battery capacity, etc.).
Nodes have limited CPU and memory capacities.
My goal is to provide WSN domain experts with tools to model "naturally" these systems and verify relevant properties (e.g. lifetime, deadlocks) without knowledge of the model-checking techniques.
Currently, I am working on VeriSensor, a Domain Specific Modeling Language for WSNs supporting formal verification and analysis. If you want to know more, please go to the Verisensor page.