Vérification formelle en temps réel de systèmes autonomes à l'aide d'un FPGA

Résumé

L'analyse d'atteignabilité de Hamilton-Jacobi est une technique puissante utilisée pour vérifier la sécurité des systèmes autonomes. Cette méthode est très efficace pour traiter la dynamique des systèmes non linéaires avec des perturbations et des représentations d'ensembles flexibles. Un inconvénient de cette approche est qu'elle souffre de la malédiction de la dimensionnalité, ce qui empêche le déploiement en temps réel sur les systèmes critiques pour la sécurité. Dans cet article, nous montrons qu'une conception matérielle personnalisée sur un FPGA (Field Programmable Gate Array) peut accélérer l'analyse d'atteignabilité de Hamilton-Jacobi (HJ) basée sur une grille 4D jusqu'à 16 fois par rapport à une implémentation optimisée et 142 fois par rapport à MATLAB ToolboxLS sur un CPU à 16 threads. Notre conception permet de surmonter le schéma d'accès aux données complexe tout en tirant parti de la nature parallèle du calcul des EDP de HJ. Grâce à cela, nous sommes en mesure de réaliser une vérification formelle en temps réel avec un modèle de voiture 4D en résolvant à nouveau l'EDP HJ à une fréquence de 5 Hz sur le FPGA lorsque l'environnement change. La latence de notre calcul est déterministe, ce qui est crucial pour les systèmes critiques en matière de sécurité. L'approche que nous présentons ici peut être appliquée à différentes dynamiques de systèmes, et de plus, potentiellement exploitée pour des systèmes de plus grande dimension. Nous démontrons également l'évitement d'obstacles avec une voiture robot dans un environnement changeant.