trier par
Copyright © 2021 ABES / OCLCListe des résultats | Notice détaillée | Où trouver ce document ?  
rechercher (et) (Mots du titre) Modélisation fonctionnelle et preuve de circuits avec LP | 1 résultat(s)

Prêt Entre Bibliothèques Prêt
Photocopie

Services  

Liens
1

Thèses (version de soutenance)

Identifiant pérenne de la notice : 
 
 
 
Type(s) de contenu (modes de consultation) :
Texte
Titre : 
Modélisation fonctionnelle et preuve de circuits avec LP / Michel Allemand ; sous la direction de Jean-Luc Paillet
Mémoire ou thèse (version d'origine)
Alphabet du titre : 
latin
Auteur(s) : 
Paillet, Jean-Luc. Directeur de thèse
Université de Provence (1970-2011). Organisme de soutenance
Date(s) : 
1995
Langue(s) : 
français
Pays : 
France
Editeur(s) :
Marseille : [s.n.], 1995
Description : 
221 f ; 30 cm
Num. national de thèse : 
1995AIX11015
 
 
Thèse : 
 
Résumé(s) : 
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
 
 
 
Titre(s) traduit(s) ajouté(s) par le catalogueur : 
FUNCTIONAL MODELISATION AND PROOF OF CIRCUITS WITH LP (anglais)
 
Sujets : 
Forme ou Genre : 
 
 
Origine de la notice : 
SF
 
Liens externes
Worldcat :