Vérification de circuits dans Coq / par Line Jakubiec ; sous la direction de Solange Coupet Grimal

Bibliogr. p. 141-147. Index

Thèse de doctorat informatique 1999 Aix-Marseille 1

La vérification formelle de circuits intégrés garantit de façon rigoureuse leur fiabilité. Pour ce faire, les assistants de preuve sont de plus en plus utilisés. Le système Coq, basé sur le Calcul des Constructions Inductives avec types co-inductifs, présente des particularités intéressantes et originales. Nous étudions ce que ce système peut apporter dans le domaine de la spécification et de la vérification de circuits. Après avoir montré l'intérêt des types dépendants pour donner des spécifications de circuits précises et donc fiables, nous utilisons le mécanisme d'extraction Coq pour synthétiser un circuit correct par construction. Nous illustrons ces aspects sur des circuits combinatoires dont l'architecture est linéaire et nous étudions sur cet exemple les diverses stratégies de preuve qu'offre Coq. Notre étude porte ensuite sur les circuits séquentiels synchrones spécifiés à l'aide de types co-inductifs. Ces types permettent de définir en Coq des objets infinis comme les streams. Les structures et les comportements des circuits sont modélisés de façon uniforme par des automates, eux-mêmes caractérisés par des fonctions co-récursives sur les streams. Notre approche est hiérarchique et modulaire et repose sur un lemme général qui exprime une équivalence entre deux streams issues respectivement de deux automates. Ce lemme prend en compte l'essentiel de l'aspect temporel de nos preuves de correction. Nous appliquons ensuite cette méthodologie à un circuit réel, le Fairisle ATM Switch Element