Post-doctorat : monitoring formel de systèmes cyber-physiques H/F

Missions :
Les systèmes cyber-physiques sont omniprésents dans nos sociétés (métros automatiques, smartphones, appareils médicaux…).
Ces systèmes doivent éviter toute erreur imprévue (bug) à même de menacer des vies, et une vérification aussi exhaustive que possible est souhaitable.
Pour les systèmes cyber-physiques pour lesquels une vérification formelle complète ne serait pas envisageable (en raison d'une explosion combinatoire, ou pour les systèmes en boîte noire pour lesquels aucun modèle n'est disponible, par exemple pour des raisons de confidentialité, ou pour les systèmes basés sur des IA non fiables), appliquer des techniques de vérification légère, telles que le monitoring, est une option très intéressante.
Un challenge est de formaliser des requêtes complexes telles que « le véhicule est toujours à une distance minimale des autres véhicules, avec la consommation énergétique maintenue sous un seuil prédéfini (où ce seuil n'est pas nécessairement connu a priori), sauf en cas de danger exceptionnel au plus une minute par heure » ; puis d'en détecter la violation sur d'énormes quantités de données.
Ceci implique d'être à même de définir des formalismes quantitatifs expressifs, ainsi que des algorithmes de vérification efficace.
Ce sujet de post-doctorat s'inscrit dans ce cadre, avec un versant tant théorique qu'algorithmique / implémentation.

Activités :
- proposition de formalismes expressifs (logiques, automates) à même d'exprimer des valeurs quantitatives dans de multiples dimensions (temps, coûts, énergie, etc.)
- proposition d'algorithmes efficaces de monitoring
- implémentation

Contexte de travail :
Le post-doc se déroule au sein du LIPN (Université Sorbonne Paris Nord), au sein de l'équipe LoVe (Logique et Vérification), axe vérification.
L'équipe LoVe compte une vingtaine de membres permanents, et plusieurs doctorants, post-doctorants et ingénieurs de recherche.