Normal view MARC view ISBD view

Modélisation fonctionnelle et preuve de circuits avec LP / Michel Allemand ; sous la direction de J.-L. Paillet

Auteur principal : Allemand, Michel, 1967-, AuteurAuteur secondaire : Paillet, Jean-Luc, 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.], 1995Description : 1 vol. (221 p.) ; 30 cmBibliographie : Bibliogr. p.155-164.Sujet MSC : 68Q42, Computer science -- Theory of computing, Grammars and rewriting systems
68Q45, Computer science -- Theory of computing, Formal languages and automata
68Q60, Computer science -- Theory of computing, Specification and verification (program logics, model checking, etc.)
97A70, Mathematics education - General, mathematics and education, Theses and postdoctoral theses
Note de thèse: Thèse de doctorat, informatique, 1995, 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 ALL (Browse shelf) Available 00754-01

Bibliogr. p.155-164

Thèse de doctorat informatique 1995 Aix-Marseille 1

Les méthodes formelles présentent des potentialités intéressantes dans le cadre de la vérification de la correction des systèmes digitaux. Cette thèse propose un système formel, le P-calcul, permettant une modélisation fonctionnelle des circuits orientée vérification formelle. Des méthodologies de preuves adaptées au démonstrateur utilisé, le Larch-Prover (LP) ainsi qu'a cette modélisation sont décrites. Dans une première partie, nous définissons un langage typé permettant de décrire les structures des circuits. Nous en donnons ensuite une interprétation dans un modèle fonctionnel, qui représente les comportements associés. Les règles de transformations que nous avons proposées sous la forme d'un système de réécriture permettent l'obtention d'une forme normale pour les expressions du langage. On peut alors, entre autre, définir un procédé de reconnaissance des circuits synchrones et donner un algorithme de construction des solutions des équations récursives décrivant les circuits avec boucles. Puis, les expressions du P-calcul sont traduites dans la syntaxe du Larch-Prover. Après avoir construit une base de propriétés arithmétiques prouvées, nous proposons deux méthodes pour vérifier que l’implémentation d'un circuit est correcte, selon que sa spécification est une définition inductive ou une liste de propriétés, et dans ce dernier cas elle n'est pas forcément complète. Ces méthodes sont appliquées à plusieurs circuits qui ont été proposés, ces dernières années, dans la communauté internationale

There are no comments for this item.

Log in to your account to post a comment.