Antoine Girard, ERC Consolidator Grant 2016

À l’heure actuelle, le développement des systèmes cyber-physiques est une tâche très complexe, qu’il s’agisse d’un robot, du régulateur de vitesse d’une automobile, ou du système de pilotage automatique d’un avion. En effet, beaucoup de temps et de multiples expertises sont nécessaires pour maitriser l’étroite interaction entre le domaine numérique et le domaine physique. 

Un des objectifs de l’ERC PROCSYS est de proposer un langage permettant de décrire les comportements d’un système cyber-physique à un niveau élevé d’abstraction, c’est-à-dire sans inclure tous les détails techniques qui sont induits. Un second objectif est de développer des algorithmes pour générer automatiquement des contrôleurs qui implémentent le comportement spécifié grâce au langage de haut niveau. Ainsi le langage spécifie le comportement du système cyber-physique, c’est-à-dire du couple système physique-contrôleur informatique, et le contrôleur généré automatiquement va, à travers son interaction avec le système physique, maintenir le comportement du système cyber-physique comme spécifié. 

Pour que cela fonctionne, il faut avoir une bonne connaissance de la dynamique du système physique, décrite par un modèle mathématique. C’est sur la base de ce modèle que des contrôleurs peuvent être synthétisés par des méthodes formelles, apportant la preuve que le comportement spécifié grâce au langage de haut niveau est correctement implémenté. Cette jonction entre l’automatique et les méthodes formelles est justement un des atouts d’Antoine Girard. 

Toutefois, les algorithmes des méthodes formelles ne fonctionnent pas directement sur les équations différentielles qui décrivent un système physique (et continu). Ce problème peut être résolu grâce au recours à des modèles symboliques. Il s’agit de représentations mathématiques discrètes du système physique, comme par exemple des automates. Les modèles symboliques sont compatibles avec les méthodes formelles et permettent ensuite de synthétiser les contrôleurs du système cyber-physique, par un retour du discret au continu. 

Les challenges à relever pour réaliser ce projet sont nombreux. Tout d’abord, il s’agit de trouver le délicat compromis entre un langage qui soit suffisamment riche et intuitif pour exprimer les subtilités souhaitées, et le besoin d’algorithmes efficaces pour la génération automatique des contrôleurs. En effet, plus le langage est riche et permet des actions variées, plus la synthèse des contrôleurs est difficile. 

Une autre problématique concerne le passage à l’échelle des systèmes physiques, et donc des algorithmes de synthèse. En effet, plus le système physique est grand et complexe, plus les modèles symboliques sont conséquents et la génération des contrôleurs coûteuse en temps et en mémoire. Antoine Girard souhaite ainsi travailler autour du calcul des modèles symboliques, pour réussir à les rendre plus compacts. Il désire également se pencher sur la synthèse des contrôleurs en développant des algorithmes, basés sur un calcul partiel des modèles symboliques, et n’explorant leur dynamique que sur les parties nécessaires au contrôle. Enfin, l’aspect robustesse est un enjeu majeur. En effet, la génération des contrôleurs se base sur des descriptions mathématiques du système physique, certes les plus précises possibles, mais qui ne sont qu’une approximation de la réalité. De quelles marges d’erreur de modélisation dispose-t-on ? Que se passe-t-il lorsque le comportement du système physique dévie de ce que prédit le modèle ? L’objectif est ainsi de déterminer dans quelle mesure le système peut être en décalage avec le modèle sans que le comportement spécifié ne soit affecté. De plus, si l’écart avec le modèle devient trop grand, par exemple en raison de perturbations non prévues par le modèle, il est nécessaire d’avoir une dégradation lisse de la qualité du fonctionnement, sans décrochage qui amènerait à des problèmes.