Normal view MARC view ISBD view

Méthodes pour la vérification formelle de systèmes matériels et logiciels à architecture régulière / par Eric Gascard ; sous la direction de Laurence Pierre

Auteur principal : Gascard, Eric, 1973-, AuteurAuteur secondaire : Pierre, Laurence, 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.], 2002Description : 1 vol. (VIII-196 p.) : fig. ; 30 cmSujet MSC : 68Mxx, Computer science - Computer system organization
68Q60, Theory of computing, Specification and verification
68V15, Computer science support for mathematical research and practice, Theorem proving
68U05, Computing methodologies and applications, Computer graphics; computational geometry
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique, 2002, 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 GAS (Browse shelf) Available 01464-01

Thèse de doctorat informatique 2002 Aix-Marseille 1

Le cadre de cette thèse est l'utilisation des méthodes formelles pour la spécification et la validation de systèmes matériels et logiciels. Nos travaux se sont concentrés sur la validation formelle de systèmes à architecture régulière et paramétrable, circuits combinatoires itératifs d'une part, et applications distribuées s'exécutant sur des réseaux d'interconnexion symétriques d'autre part. La première partie de cette thèse est consacrée à la vérification formelle automatique de circuits à structure répétitive régulière. Un modèle de fonctions récursives est utilisé, le processus de preuve mettant en jeu des techniques inductives permet un raisonnement générique sur la taille du circuit. Le résultat présenté ici est une heuristique de généralisation de théorèmes inductifs spécialisée pour les modèles fonctionnels considérés. Cette méthode permet de produire les théorèmes généralisés ainsi que certains lemmes intermédiaires et d'automatiser ainsi le processus de vérification. La seconde partie propose une méthode de modélisation et de validation de programmes distribués sur les réseaux d'interconnexion symétriques. Les preuves sont ici paramétrées sur l'ordre du réseau (nombre de processeurs). Le modèle formel choisi pour la représentation des réseaux dans l'environnement de démonstration automatique est basé sur le concept de graphe de Cayley. Notre méthode prend en compte les opérations de communications collectives (diffusion, distribution, réduction) utilisées par les applications distribuées. La modélisation et la méthode de preuve développées permettent entre autres de s'abstraire du problème des communications point à point, et de raisonner au niveau du processeur. De plus, elle permet d'obtenir automatiquement les invariants nécessaires au preuves

There are no comments for this item.

Log in to your account to post a comment.