Networks of Static and/or Mobile sensors (that is, robots) recently received significant attention from mainstream news media. Indeed, the era of expensive robots that are dedicated to a single task is past. Nowadays the tendency is to deploy networked mobile sensors that are able to execute collectively various complex tasks. One possible application of these networks could be for example to optimise the coverage of interest zones under natural or human disaster, and help in search and rescue tasks. In rescue situations, rescue people have to work rapidly to be able to save victims, but they are often limited by insufficient man-power, by their inability to reach confined spaces and by the lack of information about the location and condition of victims. In this context, networked mobile sensors can be a valuable asset to the human search and rescue teams.
The characteristic feature of mobile sensor networks is the extreme dynamism of their structure, content, and load. In these systems, nodes may join, leave and change their physical position at will with a strong impact on the system topology. Moreover, the energy fluctuation of their batteries also induces high system dynamism (that is, the system size and topology are likely to change during any computation that might take place).
Our project aims to propose a formal provable framework based on recent advances in automated proving and related areas in order to prove the correctness of localised distributed protocols in dynamic mobile sensor networks. So far, the correctness of these systems was partially explored either via restrictive simulations and experiments or via analytical tools built on top of restrictive assumptions (for example, the nodes characteristics and status do not change during the whole system execution, etc.). These assumptions may be completely unrealistic in actual networks and thus disastrous in practice. The correctness proofs of aforementioned systems should be based on a well-founded theoretical model, able to encapsulate the dynamic behaviour of these systems that must withstand frequent changes.
The Pactole project started as Digiteo Project #2009-38HD.
See also SAPPORO.
Contact: Xavier Urbain.
Main dev.: Lionel Rieg.