GT HiFi : Méthodes Formelles et Programmation Haute Fidélité pour Systèmes Critiques Émergents
Description
Les méthodes formelles ont été élaborées depuis de nombreuses années afin d’assurer un niveau aussi élevé que possible en matière de précision et de fiabilité et ont ainsi montré que l’objectif du zéro-faute est réalisable pour des systèmes dits "fermés" (qui fonctionnent dans un environnement complètement maîtrisé). Cependant, les systèmes informatiques qui émergent aujourd’hui sont de plus en plus ouverts sur des environnements plus incertains, à temps continus ou basés sur de l’apprentissage de jeux de données difficilement prédictible. En outre, grâce aux progrès réalisés dans la miniaturisation des circuits intégrés et leur autonomie, de plus en plus de systèmes ouverts sont implémentés par des programmes complexes s’exécutant sur des circuits programmables qui s’apparentent à de véritables mini-ordinateurs (microcontrôleurs, FPGA, System on Chip). On retrouve ainsi ces programmes embarqués un peu partout dans les objets de notre quotidien, dans les smartphones ou l’électroménager, mais également dans les appareils médicaux, les voitures, les avions, etc.
La complexité de ces systèmes est évidente et la maîtrise des risques inhérents à leur utilisation est ainsi de plus en plus pressante. Il est clair que pour garantir leur sûreté et leur sécurité, l’adoption de moyens d’investigation indubitables et des techniques sûres et fiables reposant sur des fondements mathématiques s’impose. Aussi, les méthodes formelles ont-elles vocation à jouer un rôle d’envergure dans ce cadre avec des bénéfices indéniables. Ce faisant, pour être efficaces, les méthodes formelles devront inévitablement s’adapter au caractère ouvert, imprécis et intelligent de ces systèmes. Ce groupe vise à faire progresser la science informatique, en particulier les méthodes formelles, pour la conception, la programmation et la vérification de ces systèmes critiques émergents.
Mots clés : Méthodes formelles (model checking, tests, interprétation abstraite, preuve, solveur SMT), Modèles (Event-B, Matlab/Simulink, Scade,...), Systèmes hybrides, Hardware programmable
Porteurs du GT
- Conchon Sylvain, LRI - VALS, Université Paris-Saclay
- Hurault Aurélie, IRIT - ACADIE, Toulouse
Animations
- Réalisation d'une liste de diffusion pour animer le groupe
- Une réunion annuelle (en plus de la session aux journées du GDR GPL) en donnant la priorité aux industriels
- Présentations régulières en visioconférence (résultats intéressants présentés ou vus en conférence, appris auprès d'un industriel,...)
- Favoriser les liens entre les doctorants du domaine : forum de discussion, rencontres en présentiel ou distanciel, ...
- Favoriser les liens entre les équipes du domaine : échange d'étudiants
Equipes
Les équipes impliquées sont :
- ACADIE, IRIT, Toulouse
- Les membres du futur LMF (Laboratoire de Méthodes Formelles) de l'Université Paris- Saclay
- SVS, LACL, Université Paris-Est Créteil
- DTIS, ONERA, Toulouse
- VASCO, LIG, Grenoble
- MaREL, LIRMM, Montpellier
- AeLoS, LS2N, Nantes
- Samovar, Evry
- Mosel, LORIA, Nancy
- U2IS, ENSTA Paris
- Équipe Parkas, INRIA Paris
- Équipe APR, LIP6, Sorbonne Université
- LAMPS, Université de Perpignan via Domitia
- Équipe LII, ENAC
- MoVe, LIP6, Paris
- Laboratoire I3S / Inria Sophia Antipolis Méditerranée
- EN COURS DE CONSTRUCTION
Interactions
Ce GT est, en parti, issu de l'ancien GT MFDL (Méthodes Formelles dans le Développement Logiciel). Les collaborations existantes entre le GT MFDL et le GT AFSEC (Approches Formelles des Systèmes Embarqués Communicants) continueront, si ces groupes sont reconduits.
Les réunions annuelles / visios conférences pourront être communes avec d'autres groupes du GDR GPL notamment :
- GT Génie Logiciel et Intelligence Artificielle (GLIA)
- GT CLAP
- GT Ingénierie des Exigences (IE)
- GT Langages et Vérification de Programmes (LVP)
- GT Méthodes de test pour la validation et la vérification (MTV2)
voir avec d'autres GDR :
- le GDR Aspects Formels et Algorithmiques de l'Intelligence Artificielle (IA)
- le GDR Informatique Mathématique (IM)