Publications

Thèses


< retour aux thèses

« Vérification formelle concluante des propriétés de systèmes multi-horloges ».

Auteur : G. Plassan
Directeur de thèse : D. Borrione
Co-directeur de thèse : K. Morin-Allory , H.-J. Peter
Président du jury : N. Halbwachs
Rapporteur(s) de thèse : J.-P. Talpin, W. Kunz,
These de Doctorat Université Grenoble Alpes
Spécialité : Informatique
Soutenance : 28/03/2018
ISBN : 978-2-11-129240-6

Résumé

Les circuits microélectroniques récents intègrent des dizaines d'horloges afin d'optimiser leur consommation et leur performance. Le nombre de traversées de domaines d'horloges (CDC) et la complexité des systèmes augmentant, garantir formellement l'intégrité d'une donnée devient un défi majeur. Plusieurs problèmes sont alors soulevés : configurer le système dans un mode réaliste, décrire l'environnement par des hypothèses sur les protocoles, gérer l'explosion de l'espace des états, analyser les contre-exemples, dots La première contribution de cette thèse a pour but d'atteindre une configuration complète et réaliste du système. Nous utilisons de la vérification formelle paramétrique ainsi qu'une analyse de la structure du circuit afin de détecter automatiquement les composants des arbres d'horloge. La seconde contribution cherche à éviter l'explosion de l'espace des états en combinant des abstractions localisées du circuit avec une analyse de contre-examples. L'idée clé est d'utiliser la technologie de raffinement d'abstraction guidée par contre-exemple (CEGAR) où l'utilisateur influence la poursuite de l'algorithme en se basant sur des informations extraites des contre-exemples intermédiaires. La troisième contribution vise à créer des hypothèses pour des environnements sous-contraints. Tout d'abord, contre-exemples sont générés pour une assertion, avec différentes raisons d'échec. Ensuite, des informations y sont minées et transformées en hypothèses réalistes. Au final, cette thèse montre qu'une vérification formelle concluante peut être obtenue en combinant la rapidité de l'analyse structurelle avec l'exhaustivité des méthodes formelles.

pdf pdf