Clavière, Arthur
[VerfasserIn]
;
Toulouse, ISAE
[MitwirkendeR];
Pagetti, Claire
[MitwirkendeR];
Asselin, Eric
[MitwirkendeR]
Vérification de la sûreté des systèmes basés réseaux de neurones s'appuyant sur les méthodes formelles ; Safety verification of neural network based systems using formal methods
Titel:
Vérification de la sûreté des systèmes basés réseaux de neurones s'appuyant sur les méthodes formelles ; Safety verification of neural network based systems using formal methods
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Contexte: la thèse a porté sur l'étude et la vérification de la sûreté de fonctionnement de systèmes contrôlés par réseaux de neurones. Ce type de système combine un système physique et un contrôleur basé réseaux de neurones. L'utilisation de ce type de contrôleur peut avoir differents intérêts: (1) approximer un autre contrôleur, déjà existant, mais en demandant moins de ressources de calcul (sachant qu'un contrôleur dispose souvent de ressources limitées) ou (2) reproduire le comportement d'un humain (ce qui peut s'avérer intéressant pour les systèmes autonomes). Dans le cas où le système contrôlé par réseaux de neurones est critique i.e., une défaillance de ce système peut entraîner des conséquences graves, alors il est important de vérifier sa sûreté de fonctionnement i.e., montrer qu'il n'atteint pas d'états non sûrs.Hypothèses: Dans la lignée des cas d'études présents dans la littérature, nous avons restreint notre étude à une forme particulière de contrôleur basé réseaux de neurones : un classificateur basé sur un ou plusieurs réseaux de neurones. Par ailleurs, nous avons considérés uniquement des réseaux de neurones feed-forward fully connected avec des fonctions d'activation ReLU.Exemple: un exemple typique de ce type de système est l'ACAS Xu qui comprend un contrôleur basé réseaux de neurones dont le rôle est d'éviter une collision entre deux avions. Pour ce système, le contrôleur basé réseaux de neurones approxime un autre contrôleur mais avec une empreinte mémoire très réduite. C'est un système critique car une défaillance peut entraîner une collision.Contributions: Afin de démontrer la sûreté de fonctionnement du système d'intérêt, nous avons d'abord considéré le cas où le contrôleur basé réseaux de neurones approxime un autre contrôleur. Pour ce cas de figure, nous avons développé une méthode et un outil afin de comparer les deux contrôleurs et montrer que le contrôleur basé réseaux de neurones est une approximation correcte du contrôleur cible. Notre méthode et notre outil ont été appliqués à ...