Langage et génie logiciel

L'agenda de recherche de D4 est de fournir les bases scientifiques et la technologie d'accompagnement pour construire des logiciels et des systèmes sûrs, sécurisés et efficaces. La convergence récente entre les logiciels embarqués et les systèmes cyberphysiques induit également de nouveaux défis en termes d'autogestion et de sécurité, en plus des questions traditionnelles d'efficacité et de correction fonctionnelle.

Il en résulte deux grands axes de travail

• l'ingénierie des systèmes/logiciels basée sur des modèles ;
• la vérification et l'analyse des programmes vérifiés par machine.

Principales contributions

• Approches logiques de la vérification des systèmes cyberphysiques : synthétiseur d'ordonnancement à source ouverte, polyvalent, appelé ADFG (affine data-flow graphs) utilisant des ILP ; vérification de programmes basée sur la preuve/le type avec des méthodes d'analyse et d'inférence basées sur une interprétation abstraite afin de proposer des méthodes d'analyse statique modulaire qui utilisent des types riches pour exposer les propriétés des modules de programmes analysés ;
• Génie logiciel et système de modélisation des systèmes : système de types avancés pour la manipulation de modèles de manière polymorphe à travers différentes DSL ; méta-modèle d'interfaces un nouveau modèle d'implémentation de langage qui permet une extensibilité indépendante de la syntaxe et de la sémantique des langages logiciels basés sur des métamodèles ; utilisation de techniques d'apprentissage machine pour mieux comprendre la variabilité existante d'une ligne de produits logiciels ; conception d'un langage de description d'architecture pour les systèmes de systèmes
• Vérifier et prouver la sécurité des logiciels : format sémantique pour l'écriture de la sémantique opérationnelle ; analyse statique pour prouver l'exécution en temps constant du code C critique et protéger contre les attaques des canaux latéraux ; amélioration de l'analyse statique et extension aux approches hybrides combinant l'analyse statique et la surveillance de l'exécution ; vérification des propriétés de sécurité des systèmes d'architecture des systèmes
• Modélisation du système : contributions théoriques sur la diagnosticabilité et la diagnosticabilité approximative ; algorithmes de synthèse pour les moniteurs d'application de la loi à partir d'automates temporisés ; contributions à la synthèse et au contrôle des systèmes de la théorie des jeux ; modélisation des systèmes centrés sur les données avec les réseaux de Petri ; résultats fondateurs sur l'analyse structurelle des systèmes d'équations algébriques différentielles multimodes ;