Verification formelle bout-en-bout d'algorithmes de contrôle – CAFEE

La conception de systèmes de contrôles par les automaticiens est
principalement centrée sur le comportement à haut niveau des
algorithmes de contrôle, caractérisant leurs propriétés comme la
stabilité ou convergence, la robustesse et la performance. En
particulier, ils supposent généralement que tous les calculs sont
effectués avec des nombres réels et la problématique de l'exécution
sur une machine physique ou même la programmation de loi de contrôle,
en encore la prise en compte des erreurs de calculs liées à
l'utilisation d'une arithmétique à précision finie, restent souvent
négligés. Dans le projet CAFEE, nous visons à combler le fossé entre
la théorie du contrôle et les implémentations de bas niveau, en
fournissant des garanties typiques de la théorie du contrôle sur
l'implémentation plutôt que sur un algorithme de haut niveau.

Le projet CAFEE vise donc à réaliser une vérification complète de bout
en bout des systèmes de contrôle, depuis des modèles haut-niveau qui
combinent contrôleurs et modélisation physique du système par des
équations différentielles, jusqu'à la vérification de code C embarqué
dans ces systèmes.


--- Contributions

Le projet CAFEE est structuré en 5 lots de travaux différents. De façon préliminaire, nous construirons une approche intégrée pour les systèmes linéaires à temps discret, en proposant un processus de bout en bout permettant la vérification à toutes les étapes, du modèle au code, avec une sémantique à temps discret pour modéliser le système. Ensuite, nous étudierons deux extensions. D'une part, nous étendrons l'approche aux systèmes hybrides composés d'une dynamique à temps continu pour modéliser la partie physique et d'une dynamique de contrôleur à temps discret. Alors que les ingénieurs en contrôle travaillent généralement avec des modèles à temps continu ou à temps discret à des fins de vérification, le système réel combine les deux paradigmes. Nous définirons un modèle sémantique approprié pour ces systèmes hybrides et développerons de nouveaux moyens de vérification pour raisonner sur ces systèmes en boucle fermée. L'autre extension se focalisera spécifiquement sur les algorithmes de contrôle qui reposent sur des routines d'optimisation, en ligne. Peu de travaux de vérification ont été réalisés dans ce contexte, et nous prévoyons d'exploiter certains de nos travaux récents et de développer des techniques de vérification qui pourront être appliquées à de telles routines d'optimisation.

Ces différentes propositions seront intégrées dans un quatrième lot, avec un focus particulier sur les enjeux autour de la précision numérique en utilisant l'arithmétique machine, ainsi que l'optimisation de cette dernière. La vérification sera ensuite effectuée au niveau du modèle et tout au long du cycle de développement, en s'appuyant sur l'autocodage et en ciblant la plate-forme matérielle finale, tout en tenant compte de la précision numérique du calcul. Un dernier lot cherchera à mettre en oeuvre méthodes et outils sur trois cas d'étude différents: un algorithme de prévention des collisions automobiles, un algorithme de contrôle de drone et un cas d'étude spatial, comme par exemple l'amarrage d'engins spatiaux.

--- Impacts

Le projet CAFEE permettra de définir un cadre formel permettant la vérification de bout en bout des algorithmes de contrôle. Ces outils seront diffusé avec un modèle open-source et pourront être utilisé par des partenaires académiques, gouvernementaux et industriels. Nous intégrerons également l'utilisation de ces méthodes et outils dans les enseignements à l'ENAC et à l'Université du Michigan.

Un autre impact plus large du projet sera de rapprocher la communauté des méthodes formelles et la communauté traditionnelle de la théorie du contrôle. En rapprochant ces communautés, nous espérons sensibiliser la communauté du contrôle à des questions logicielles telles que l'arithmétique des langages de programmation et la précision des machines.