Normal view MARC view ISBD view

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

Auteur principal : Jakubiec, Line, AuteurAuteur secondaire : Coupet-Grimal, Solange, 1952-, Directeur de thèseAuteur secondaire collectivité : Université de Provence, Etablissement de soutenanceType 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 proving
68Q45, Theory of computing, Formal languages and automata
68Q60, Theory of computing, Specification and verification
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique, 1999, Aix-Marseille 1
Tags from this library: No tags from this library for this title. Log in to add tags.
Current location Call number Status Date due Barcode
CMI
Salle S
Thèses JAK (Browse shelf) 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 for this item.

Log in to your account to post a comment.