The description of the work to be done will be detailed later. Feel free to contact mailto:Florence.Maraninchi@imag.fr for more details if you are interested.
Sensor networks are essentially distributed systems. Each node has its own hardware clock. The various protocols that are developed for sensor networks (from the MAC level to the routing level), use time a lot (each node counts delays on its own clock) in order to agree on the periods of time when they can communicate.
On the other hand, it is well known that the various hardware clocks in a distributed system are not synchronized, unless a special clock-synchronization protocol is implemented.
In order to validate this kind of clock-synchronization protocols, we need a model of their execution platform, i.e., a realistic model of how clocks may diverge in a distributed system. Once we have such a model, we can :
- simulate the behavior of the synchronization protocol
- perform automatic testing
- apply formal verification techniques (model-checking, abstract-interpretation, ...)
- use it together with a MAC protocol, in order to validate the fact that the MAC protocol, although it uses time counters, is somewhat robust enough to tolerate the amount of de-synchronization that is unavoidable, even with a clock-synchronization protocol.
For a survey on synchronization protocols, see this paper.
Expected Work
- Bibliography on clock synchronization protocols in wireless sensor networks
- Modeling of one protocol on top of an existing model of hardware clocks (developed in the group). This will done by reusing a method that has been applied for the development of a MAC protocol.
- Proposals for the validation of this protocol, alone
- Integration of the synchronization protocol with upper layer protocols (typically the MAC layer).
Expected Skills and Background
- Programming
- Notions on Network Protocols (but this can be acquired during the internship)
- Ability to deal with formal specifications (automata, logics, ...)
The necessary knowledge about formal verification will be provided in the "Embedded Systems" course of the MOSIG programme.
