Formal methods for Programming and Analysis of Robust Behaviors of Autonomous Systems
Supervisors: LESIRE-CABANIOLS Charles (ONERA/DTIS, Univ. Toulouse), GODARY-DÉJEAN Karen, LIRMM, Univ Montpellier-CNRS
Location: Main location : ONERA, Toulouse ; Secondary location : LIRMM, Montpellier.
Duration: 3 years.
Requirements: Programming skills, notions in formal methods.
The development of autonomous robotic systems involves intelligent functionalities, such as system control, data processing, or trajectory planning. The implementation of these functionalities results in complex software architectures, involving dozens of processes. The realization of critical missions in autonomy, such as the exploration of marine ecosystems in order to acquire data on biodiversity, requires the ability to specify high-level behaviors that are robust to the occurrence of unexpected events (failures, obstacles, ...). This thesis aims at proposing a programming environment for autonomous systems based on formal methods, in order to ensure and formally demonstrate the robustness of the system. This work will be based on previous work developed at ONERA and LIRMM, and will aim at an application of underwater robotics for the monitoring of marine biodiversity in strategic regional sites.