Post-doctorant : veille formelle de systèmes cyberphysiques

Les systèmes cyber-physiques sont omniprésents dans notre société (métros automatisés, smartphones, dispositifs médicaux, etc.).
Ces systèmes doivent éviter toute erreur imprévue (bug) pouvant menacer des vies, et une vérification formelle aussi exhaustive que possible est fortement souhaitée.
Pour les systèmes cyber-physiques pour lesquels une vérification formelle complète n’est pas réalisable (en raison d’une explosion combinatoire de l’espace d’états, ou pour les systèmes de 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 une IA peu fiable), l’application de méthodes légères les techniques de vérification, comme le monitoring, constituent une option très intéressante.
Un enjeu est de formaliser des demandes complexes telles que « le véhicule soit toujours à une distance minimale des autres véhicules, avec une consommation d’énergie maintenue en dessous d’un seuil prédéfini (où ce seuil n’est pas forcément connu a priori avec précision), sauf en cas de danger exceptionnel au maximum une minute par heure» ; puis de détecter d’éventuelles violations de ces requêtes sur d’énormes quantités de données.
Cela implique de pouvoir définir des formalismes quantitatifs expressifs, ainsi que des algorithmes de vérification efficaces.
Ce sujet de post-doctorat s’inscrit dans ce cadre, avec à la fois des aspects théoriques et algorithmiques/mise en œuvre.

– proposer des formalismes expressifs (logiques, automates) capables d’exprimer des valeurs quantitatives dans de multiples dimensions (temps, coût, énergie, etc.)
– proposer des algorithmes de surveillance efficaces
– mettre en œuvre ces algorithmes et les évaluer par rapport à des benchmarks

Le poste post doc se déroulera au laboratoire LIPN (Université Sorbonne Paris Nord), dans l’équipe LoVe (Logique et Vérification), dans la sous-équipe «Vérification».