An emergent trend has recently received significant attention: networks of passively and/or actively mobile sensors (that is, swarms of robots). These robots are able to execute collectively various complex tasks; one application being for example to optimise the coverage of interest zones under natural or human disaster, and help in search and rescue tasks. A characteristic feature is the extreme dynamism of their structure, content, load, and even execution environment. Possibly the subjects to Byzantine failures, obtaining certified guarantees on they behaviour is a crucial issue, as they belong to an area of computer science well-known for being remarkably harsh on informal reasoning, possibly leading to disastrous errors when arguments are not perfectly clear.
Project SAPPORO aims to propose a formal provable framework (mechanised in the Coq proof assistant) to assess the correctness of localised distributed protocols at the core of dynamic mobile sensor networks.
It relies on the Pactole framework and formal libraries we develop.