Formal rule-based scenarios for the design of safe autonomous vehicles

Scénarios formels basés sur des règles pour la conception de véhicules autonomes sûrs Les constructeurs automobiles se préparent à déployer des flottes de Véhicules Autonomes (VAs). Cela soulève des défis à la fois techniques et sociaux. En effet, l'acceptation tant par les usagers que par les pouvoirs publics nécessite de convaincre de la sûreté, de la fiabilité, et de la sécurité des solutions proposées. Les erreurs majeures commises par les AV ne peuvent être tolérées par la société, qui attend une politique proche du zéro accident. Compte tenu de la grande incertitude dans l'environnement des VAs, nous ne pouvons pas nous contenter d'utiliser uniquement les techniques de vérification systématiques et exhaustives. Par conséquent, nous devons nous appuyer sur l'approche hypothèse-garantie dans laquelle nous pouvons appliquer certaines garanties sur la sûreté de fonctionnement du véhicule à partir d'un ensemble d'hypothèses sur l'environnement. Ce travail aborde ce sujet en considérant une approche basée sur des scénarios pour les cas dangereux connus. La sûreté de fonctionnement se limite à l'acceptation de la norme Safety Of The Intended Functionality (SOTIF), récemment définie par la norme ISO/PAS 21448. Une proposition pour évaluer la sûreté de fonctionnement consiste à tester des VAs en circulation réelle et à observer leur comportement. Aussi logique que cela puisse paraître, cette méthode est difficilement réalisable et largement insuffisante car elle présente des risques importants pour l'environnement et nécessite de nombreux tests. Cette méthode est donc non évolutive et non exhaustive car il n'est pas possible de couvrir tous les scénarios possibles, et notamment ceux très peu probables, avec une occurrence très faible. Ce que nous proposons, c'est de définir précisément des scénarios dans lesquels nous décrivons les conditions de l'environnement ainsi que les risques et les mesures à prendre lorsqu'un danger est identifié. Dans cette thèse, nous concevons un processus basé sur la modélisation formelle et la vérification pour donner des garanties suffisantes et construire des preuves concrètes pour assurer la sûreté de fonctionnement du VA. Nous proposons un langage formel, appelé Extensible Platform for Safety Analysis of AVs (EPSAAV), pour combler l'écart entre les exigences de sûreté de fonctionnement, généralement exprimées en langage naturel, et le code réel intégré à l'intérieur du véhicule. Nous utilisons EPSAAV comme Model-Based System Engineering (MBSE) dans une approche centrée sur des modèles où les artefacts et les analyses sont automatiquement dérivés du modèle. Nous proposons trois instanciations de ce langage. Dans un premier temps, nous générons un rapport de sûreté de fonctionnement qui peut servir de référence au niveau de l'entreprise pour diffuser la politique de sûreté de fonctionnement à appliquer dans l'entreprise. Dans un second temps, nous générons un moniteur dédié pour s'interfacer avec un simulateur choisi. La sémantique opérationnelle de ce moniteur est exploitée en simulation pour déboguer et identifier les ambiguïtés dans les scénarios. Typiquement, cela peut être utilisé par d'autres équipes pour valider leur travail par rapport à la politique de sûreté de fonctionnement globale de l'entreprise. Troisièmement, nous nous appuyons sur la sémantique formelle de ce langage pour détecter les incohérences pouvant découler des exigences de sûreté de fonctionnement. À cette fin, nous construisons un moteur de vérification dédié. Enfin, pour illustrer la faisabilité de l'approche proposée, nous l'appliquons à la politique de sûreté de fonctionnement Renault-Nissan pleinement intégrée aux équipes opérationnelles du groupe Renault.