Informations générales
Intitulé de l'offre : Post-doctorat : monitoring formel de systèmes cyber-physiques H/F
Référence : UMR7030-ETIAND-002
Nombre de Postes : 1
Lieu de travail : VILLETANEUSE
Date de publication : mercredi 21 février 2024
Type de contrat : CDD Scientifique
Durée du contrat : 12 mois
Date d'embauche prévue : 1 juin 2024
Quotité de travail : Temps complet
Rémunération : Base brut standard : comprise entre 2932,85 euros brut mensuel et 3371,38 euros brut mensuel pour une personne en CDD de moins de 2 ans d'expérience
Niveau d'études souhaité : Niveau 8 - (Doctorat)
Expérience souhaitée : Indifférent
Section(s) CN : Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations
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
Compétences
Une expertise dans un ou plusieurs domaines suivants sera appréciée :
- monitoring
- model checking
- logiques temporelles
- automates temporisés
- automates temporisés paramétrés
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.
Contraintes et risques
N/A
Informations complémentaires
Embauche possible à tout moment, et au plus tard en septembre 2024