Analyses formelles et exhaustives de systèmes embarqués de contrôle à base de calculs intensifs – FEANICSES

Avec le développement de la capacité des calculateurs, tant en puissance de
calcul qu'en mémoire, on observe un intérêt croissant pour les fonctions
embarquées numériques avancées. Cependant les coûts de vérification et
validation croient eux de façon exponentielle et posent aujourd'hui une barrière
quant à l'adoption de ces nouveaux systèmes. Il est ainsi de notoriété publique
que la moitié du coût des développements des systèmes dans un avion civil est
absorbé par la certification du logiciel. La validation d'algorithmes embarqués
avancés de calcul de trajectoire pour l'atterrissage de fusée, de ré-allocation
dynamique de surfaces de contrôle, ou d'anti-collision est donc difficile sinon
incompatible avec les capacités de certification des industriels à ce jour.

Le projet FEANICSES cherche donc à ouvrir ces verrous et proposer des nouvelles
méthodes théoriques et pratiques pour analyser les performances systèmes que
sont la stabilité, la robustesse et la performance, et ce, à tous stages de
développement de ces systèmes, y compris au niveau du code embarqué. Le postulat
scientifique qui sous-tend cette étude est que l'ensemble de ces propriétés est
exprimable sous la forme d'invariants numériques sur les états atteignables du
système, par exemple via l'utilisation de fonctions de Lyapunov. Les travaux
proposés consistent donc à exprimer les propriétés d'intérêt sous cette forme et
à définir de nouvelles méthodes d'analyses statiques non linéaires pour valider ces
propriétés ainsi formulées.

L'équipe interdisciplinaire proposée autour de ce projet "jeune chercheur"
rassemble des chercheurs jeunes et plus confirmés, experts à la fois des méthodes
formelles et de la mise au point et de l'analyse de ces systèmes de contrôle
avancés.

Les résultats du projet FEANICSES seront illustrés dans un démonstrateur: une
chaîne d'outils intégrés permettant d'analyser des systèmes de contrôle tout au
long de leur développement. Ce démonstrateur sera évalué sur des exemples
représentatifs, de taille industrielle. L'objectif étant à la fois d'automatiser
les analyses et de traiter des propriétés plus complexes.