Hardware acceleration of safety and liveness verification on reconfigurable architectures

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

Émilien Fournier (1, 2)

1 Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
2 Lab-STICC_ARCAD - Equipe Hardware ARchitectures and CAD tools

Model-Checking is an automated technique used in industry for verification, a major issue in the design of reliable systems, where performance and scalability are critical. Swarm verification improves scalability through a partial approach based on concurrent execution of randomized analyses. Reconfigurable architectures promise significant performance gains. However, existing work suffers from a monolithic design that hinders the exploration of reconfigurable architecture opportunities. Moreover, these studies are limited to safety verification. To adapt the verification strategy to the problem, this thesis first proposes a hardware verification framework, allowing to gain, through a modular architecture, a semantic and algorithmic genericity, illustrated by the integration of 3 specification languages and 6 algorithms. This framework allows efficiency studies of swarm algorithms to obtain a scalable safety verification core. The results, on a high-end FPGA, show gains of an order of magnitude compared to the state-of-the-art. Finally, we propose the first hardware accelerator for safety and liveness verification. The results show an average speed-up of 4875x compared to software.

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.

Mots clés: Model checking; Swarm verification; Reconfigurable architectures

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

Domaines: Génie logiciel [cs.SE]

Émilien Fournier. Accélération matérielle de la vérification de sûreté et vivacité sur des architectures reconfigurables. Génie logiciel [cs.SE]. ENSTA Bretagne - École nationale supérieure de techniques avancées Bretagne, 2022. Français. ⟨NNT : 2022ENTA0006⟩. ⟨tel-04109895⟩