Résumé de rapport du LIF

Téléchargement / Download : pdf 220k , ps.gz 192k , bibtex

Abstract

We investigate how to take advantage of the particular features of the Calculus of Inductive Constructions in the framework of hardware verification. First, we emphasize in a short case study the use of dependent types and of the constructive aspect of the logic for specifying and synthesizing combinatorial circuits. Then, co-inductive types are introduced to model the temporal aspects of sequential synchronous devices. Moore and Mealy automata are co-inductively axiomatized and are used to represent uniformly both the structures and the behaviors of the circuits. This leads to clear, general and elegant proof processes as it is illustrated on the example of a realistic circuit: the ATM Switch Fabric. All the proofs are carried out using Coq.

Keywords

Formal methods, hardware verification, type theory, dependent types, co-induction, extraction.

Résumé

Nous étudions comment tirer parti au mieux, dans le domaine de la vérification de hardware, des particularités du Calcul des Constructions Inductives. Nous nous intéressons tout d'abord, dans une courte étude de cas, aux types dépendants et à l'aspect constructif de la logique sous-jacente pour spécifier et synthétiser des circuits combinatoires. Puis nous étendons notre étude aux circuits séquentiels synchrones en introduisant des types co-inductifs pour modéliser les aspects temporels. Nous donnons une axiomatisation co-inductive des automates de Moore et de Mealy que nous utilisons pour représenter uniformément les structures et les comportements. Il en résulte des processus de preuve clairs, généraux et élégants comme nous l'illustrons sur l'exemple d'un vrai circuit: l'ATM Switch Fabric. Toutes les preuves sont vérifiées à l'aide de l'assistant de preuve Coq.

Mots clés

Méthodes formelles, vérification de hardware, théorie des types, types dépendants, co-induction, extraction.

Bibtex

@TECHREPORT{03-2002,
    AUTHOR	= {Solange Coupet-Grimal and Line Jakubiec},
    TITLE	= {{Certifying Circuits in Type Theory}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {03-2002},
    MONTH	= {May},
    YEAR	= {2002},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/03-2002.html},
}