Modélisation fonctionnelle et preuve de circuits avec LP / Michel Allemand ; sous la direction de Jean-Luc Paillet

Date :

Editeur / Publisher : Marseille : [s.n.] , 1995

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Modèles mathématiques

Circuits électroniques -- Calcul

Paillet, Jean-Luc (Directeur de thèse / thesis advisor)

Université de Provence (1970-2011) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : LES METHODES FORMELLES PRESENTENT DES POTENTIALITES INTERESSANTES DANS LE CADRE DE LA VERIFICATION DE LA CORRECTION DES SYSTEMES DIGITAUX. CETTE THESE PROPOSE UN SYSTEME FORMEL, LE P-CALCUL, PERMETTANT UNE MODELISATION FONCTIONNELLE DES CIRCUITS ORIENTEE VERIFICATION FORMELLE. DES METHODOLOGIES DE PREUVES ADAPTEES AU DEMONSTRATEUR UTILISE, LE LARCH-PROVER (LP) AINSI QU'A CETTE MODELISATION SONT DECRITES. DANS UNE PREMIERE PARTIE, NOUS DEFINISSONS UN LANGAGE TYPE PERMETTANT DE DECRIRE LES STRUCTURES DES CIRCUITS. NOUS EN DONNONS ENSUITE UNE INTERPRETATION DANS UN MODELE FONCTIONNEL, QUI REPRESENTE LES COMPORTEMENTS ASSOCIES. LES REGLES DE TRANSFORMATIONS QUE NOUS AVONS PROPOSEES SOUS LA FORME D'UN SYSTEME DE REECRITURE PERMETTENT L'OBTENTION D'UNE FORME NORMALE POUR LES EXPRESSIONS DU LANGAGE. ON PEUT ALORS, ENTRE AUTRE, DEFINIR UN PROCEDE DE RECONNAISSANCE DES CIRCUITS SYNCHRONES ET DONNER UN ALGORITHME DE CONSTRUCTION DES SOLUTIONS DES EQUATIONS RECURSIVES DECRIVANT LES CIRCUITS AVEC BOUCLES. PUIS, LES EXPRESSIONS DU P-CALCUL SONT TRADUITES DANS LA SYNTAXE DU LARCH-PROVER. APRES AVOIR CONSTRUIT UNE BASE DE PROPRIETES ARITHMETIQUES PROUVEES, NOUS PROPOSONS DEUX METHODES POUR VERIFIER QUE L'IMPLEMENTATION D'UN CIRCUIT EST CORRECTE, SELON QUE SA SPECIFICATION EST UNE DEFINITION INDUCTIVE OU UNE LISTE DE PROPRIETES, ET DANS CE DERNIER CAS ELLE N'EST PAS FORCEMENT COMPLETE. CES METHODES SONT APPLIQUEES A PLUSIEURS CIRCUITS QUI ONT ETE PROPOSES, CES DERNIERES ANNEES, DANS LA COMMUNAUTE INTERNATIONALE