Le laboratoire Verimag développe des recherches fondamentales et appliquées pour la conception de systèmes cyber-physiques sûrs et sécurisés : (1) Sémantique et validation de propriétés des programmes et des systèmes, aspects fondamentaux et développement d’outils utilisables en vraie grandeur, modèles de haut niveau et interface logiciel/matériel ; (2) Méthodes et outils d’implantation correcte et efficace des systèmes cyber-physiques : langages de programmation dédiés, compilateurs, méthodes dirigées par les modèles, composants, parallélisation et distribution, optimisation, etc. ; (3) Méthodes et outils de modélisation, analyse et simulation des comportements de l’ensemble cyber-physique : systèmes hybrides continus/discrets, architectures matérielles/logicielles, etc.
Profil de recherche :
Les systèmes cyberphysiques (CPS) devenant de plus en plus autonomes et adaptables ils sont aussi de plus en plus vulnérables à des environnements défaillants ou hostiles. De plus ils sont amenés à inclure des composants de type IA analysant ces environnements pour prendre des décisions. Dans des domaines où les CPS étaient déjà critiques, cette évolution introduit de nouveaux problèmes de sûreté, sécurité et pérennité des systèmes, en rendant plus difficiles les compromis entre le coût, la qualité et la sécurité. Ces évolutions demandent de repenser les méthodes de spécification et développement et les architectures des systèmes informatiques, pour que la validation et la certification soient toujours possibles, et que les systèmes aient une durée de vie suffisante. C’est une condition forte de l’acceptabilité des systèmes autonomes, dans tous les domaines d’application. Parallèlement, les techniques d’intelligence artificielle devenant plus mûres, on peut envisager leur usage pour guider des procédures de compilation, de preuve, de recherche de bugs, etc.
Le ou la candidat(e) retenu(e) intégrera le laboratoire Verimag et son activité de recherche pourra s’inscrire dans les directions suivantes (liste non exhaustive) :
- Outils pour l’aide au développement, la validation et la certification prenant en compte la sûreté et la sécurité pour les systèmes Cyber Physiques actuels
- Raisonnement formel sur du code en présence d’attaquants actifs pendant l’exécution, analyse de contre-mesures
- Validation et certification des systèmes comportant des composants de type IA
- Implémentations prouvées d’algorithmes IA, logicielles ou sur matériel dédié, compilateurs
- Implantations correctes par construction, approches dirigées par les modèles, prise en compte de la résilience en cas de défaillance ou d’attaques
- Test, simulation, modélisation des systèmes autonomes et de leurs environnements physiques et humains
