Vérification de circuits dans Coq / par Line Jakubiec ; sous la direction de Solange Coupet Grimal
Type de document : ThèseLangue : français.Pays: France.Éditeur : [S.l.] : [s.n.], 1999Description : 1 vol. (149 p.) : fig. ; 30 cmBibliographie : Bibliogr. p. 141-147. Index.Sujet MSC : 68V15, Computer science support for mathematical research and practice, Theorem proving68Q45, Computer science - Theory of computing, Formal languages and automata
68Q60, Computer science - Theory of computing, Specification and verification
97-02, Research exposition (monographs, survey articles) pertaining to mathematics educationNote de thèse: Thèse de doctorat, informatique, 1999, Aix-Marseille 1 Item type:

Current library | Call number | Status | Date due | Barcode |
---|---|---|---|---|
CMI Salle S | Thèses JAK (Browse shelf(Opens below)) | Available | 00253-01 |
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
There are no comments on this title.