SEGI - Systèmes embarqués et grandes infrastructures

Vérification et Conception de Systèmes Cyber-Physiques – VEDECY

Résumé de soumission

Le projet VEDECY est un projet de recherche fondamentale pour le développement d'approches algorithmiques de vérification et conception de systèmes cyber-physiques. Les systèmes cyber-physiques résultent de l'intégration de systèmes informatisés et de processus physiques : des calculateurs embarqués contrôlent des processus physiques qui à leur tour affectent les calculs par l'intermédiaire de boucles de rétroaction. Ils sont omniprésents dans la technologie moderne et leur impact sur la vie du citoyen est amené à croître dans le futur (véhicules autonomes, chirurgie robotique, bâtiment écologiquement intelligent...). Les applications des systèmes cyber-physiques sont souvent critiques du point de vue de la sûreté et, par conséquent, la fiabilité est une exigence majeure. L'utilisation d'approches basées sur des modèles et les méthodes formelles permet de fournir des assurances de fiabilité. Les modèles des systèmes cyber-physiques sont par nature hétérogènes : systèmes dynamiques discrets pour les calculs et équations différentielles continues pour les processus continus. La théorie des systèmes hybrides offre un cadre rigoureux de modélisation pour les systèmes cyber-physiques. Le but du projet VEDECY est de développer des techniques basées sur le formalisme des systèmes hybrides pour la vérification et conception des systèmes cyber-physiques. Il regroupe des experts des domaines des systèmes hybrides et des méthodes formelles qui travailleront suivant trois problématiques principales : (1) Analyse d'atteignabilité des systèmes continus : l'objectif est de calculer l'ensemble des états atteignables d'un processus physique, modélisé par un système dynamique continu. Notre but principal est de développer des approches spécifiques pour l'analyse d'atteignabilité des systèmes non-linéaires, qui passent significativement mieux à l'échelle que les techniques actuellement disponibles. (2) Vérification des systèmes cyber-physiques : l'objectif est de valider le comportement du système cyber-physique résultant de l'intégration du logiciel de contrôle-commande avec le processus physique. Pour cela, il est d'abord nécessaire de comprendre comment le logiciel se comporte en interaction avec le processus physique. Ensuite, des approches spécifiques pour l'analyse des systèmes cyber-physiques résultant seront développées. (3) Conception de contrôleurs embarqués : l'objectif est de synthétiser un modèle de contrôleur embarqué qui serait ``correct par construction'', basé sur un modèle continu du processus physique. Nous utiliserons des approches basées sur des abstractions discrètes, équivalentes ou approximativement équivalentes au système continu, qui permettent de profiter de l'éventail de méthodes disponibles pour les systèmes discrets. Aussi, une partie de notre travail sera consacrée au développement de techniques pour réduire la complexité des contrôleurs synthétisés afin de faciliter leur implémentation. Le travail sur les systèmes cyber-physiques requière en même temps des connaissances sur la dynamique du logiciel et des systèmes physiques. L'implication d'informaticiens et de mathématiciens appliqués garantit que les compétences nécessaires à l'analyse des systèmes cyber-physiques sont bien représentées dans le projet. La théorie des systèmes hybrides offre un cadre rigoureux de modélisation pour les systèmes cyber-physiques. Le but du projet VEDECY est de développer des techniques basées sur le formalisme des systèmes hybrides pour la vérification et conception des systèmes cyber-physiques. Il regroupe des experts des domaines des systèmes hybrides et des méthodes formelles qui travailleront suivant trois problématiques principales : (1) Analyse d'atteignabilité des systèmes continus : l'objectif est de calculer l'ensemble des états atteignables d'un processus physique, modélisé par un système dynamique continu. Notre but principal est de développer des approches spécifiques pour l'analyse d'atteignabilité des systèmes non-linéaires, qui passent significativement mieux à l'échelle que les techniques actuellement disponibles. (2) Vérification des systèmes cyber-physiques : l'objectif est de valider le comportement du système cyber-physique résultant de l'intégration du logiciel de contrôle-commande avec le processus physique. Pour cela, il est d'abord nécessaire de comprendre comment le logiciel se comporte en interaction avec le processus physique. Ensuite, des approches spécifiques pour l'analyse des systèmes cyber-physiques résultant seront développées. (3) Conception de contrôleurs embarqués : l'objectif est de synthétiser un modèle de contrôleur embarqué qui serait ``correct par construction'', basé sur un modèle continu du processus physique. Nous utiliserons des approches basées sur des abstractions discrètes, équivalentes ou approximativement équivalentes au système continu, qui permettent de profiter de l'éventail de méthodes disponibles pour les systèmes discrets. Aussi, une partie de notre travail sera consacrée au développement de techniques pour réduire la complexité des contrôleurs synthétisés afin de faciliter leur implémentation. Le travail sur les systèmes cyber-physiques requière en même temps des connaissances sur la dynamique du logiciel et des systèmes physiques. L'implication d'informaticiens et de mathématiciens appliqués garantit que les compétences nécessaires à l'analyse des systèmes cyber-physiques sont bien représentées dans le projet. Ensuite, des approches spécifiques pour l'analyse des systèmes cyber-physiques résultant seront développées. (3) Conception de contrôleurs embarqués : l'objectif est de synthétiser un modèle de contrôleur embarqué qui serait ``correct par construction'', basé sur un modèle continu du processus physique. Nous utiliserons des approches basées sur des abstractions discrètes, équivalentes ou approximativement équivalentes au système continu, qui permettent de profiter de l'éventail de méthodes disponibles pour les systèmes discrets. Aussi, une partie de notre travail sera consacrée au développement de techniques pour réduire la complexité des contrôleurs synthétisés afin de faciliter leur implémentation. Le travail sur les systèmes cyber-physiques requière en même temps des connaissances sur la dynamique du logiciel et des systèmes physiques. L'implication d'informaticiens et de mathématiciens appliqués garantit que les compétences nécessaires à l'analyse des systèmes cyber-physiques sont bien représentées dans le projet.

Coordination du projet

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Aide de l'ANR 0 euros
Début et durée du projet scientifique : - 0 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter