Assas Recherche | Accélération matérielle de la vérification de sûreté et vivacité sur des architectures reconfigurables

Accélération matérielle de la vérification de sûreté et vivacité sur des architectures reconfigurables (Document en Français)

Accès au(x) document(s)

Accéder au(x) document(s) :

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Modalités de diffusion de la thèse :

Thèse consultable sur internet, en texte intégral.

Informations sur les contributeurs

Auteur : Fournier E?milien

Fournier, E?milien

Nom

Fournier

Prénom

E?milien

Nationalité

Français

Date de soutenance : 05-07-2022

Directeur(s) de thèse : Lagadec Loïc

Lagadec, Loïc

Nom

Lagadec

Prénom

Loïc

Etablissement de soutenance : Brest, École nationale supérieure de techniques avancées Bretagne

Brest, École nationale supérieure de techniques avancées Bretagne

Nom

Brest, École nationale supérieure de techniques avancées Bretagne

Laboratoire : Laboratoire en sciences et techniques de l'information, de la communication et de la connaissance (Brest ; 2012-....)

Laboratoire en sciences et techniques de l'information, de la communication et de la connaissance (Brest ; 2012-....)

Nom

Laboratoire en sciences et techniques de l'information, de la communication et de la connaissance (Brest ; 2012-....)

- Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance

Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance

Nom

Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance

Ecole doctorale : École doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)

École doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)

Nom

École doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)

Informations générales

Discipline : Informatique
Classification : Informatique

Mots-clés libres : Vérification de modèles (informatique), Intelligence collective, Systèmes adaptatifs (informatique)
Mots-clés :

Conception de systèmes informatiques - Méthodes formelles (informatique)
Vérification de modèles (informatique) - Optimisation par essaims particulaires
Systèmes adaptatifs (technologie) - Réseaux logiques programmables par l'utilisateur

Résumé : Le Model-Checking est une technique automatisée, utilisée dans l’industrie pour la vérification, enjeu majeur pour la conception de systèmes fiables, cadre dans lequel performance et scalabilité sont critiques. La vérification swarm améliore la scalabilité par une approche partielle reposant sur l’exécution concurrente d’analyses randomisées. Les architectures reconfigurables promettent des gains de performance significatifs. Cependant, les travaux existant souffrent d’une conception monolithique qui freine l’exploration des opportunités des architectures reconfigurable. De plus, ces travaux sont limités a la verification de sûreté. Pour adapter la stratégie de vérification au problème, cette thèse propose un framework de vérification matérielle, permettant de gagner, au travers d’une architecture modulaire, une généricité sémantique et algorithmique, illustrée par l’intégration de 3 langages de spécification et de 6 algorithmes. Ce cadre architectural permet l’étude de l’efficacité des algorithmes swarm pour obtenir un cœur de vérification de sûreté scalable. Les résultats, sur un FPGA haut de gamme, montrent des gains d’un ordre de grandeur par rapport à l’état de l’art. Enfin, on propose le premier accélérateur matériel permettant la vérification des exigences de sûreté et de vivacité. Les résultats démontrent un facteur d’accélération moyen de 4875x par rapport au logiciel.

Informations techniques

Type de contenu : Text
Format : PDF

Informations complémentaires

Entrepôt d'origine :

STAR : dépôt national des thèses électroniques françaises

Identifiant : 2022ENTA0006
Type de ressource : Thèse