Contribution à la vérification des spécifications algébriques : application à certaines propriétés de programmes parallèles - Université de Lorraine Accéder directement au contenu
Thèse Année : 1990

Verification of algebraic specifications : application to some properties of parallel programs

Contribution à la vérification des spécifications algébriques : application à certaines propriétés de programmes parallèles

Noureddine Lazrak
  • Fonction : Auteur
  • PersonId : 787522
  • IdRef : 189520531

Résumé

Not available
Notre objectif dans cette thèse est de vérifier la validité d'une formule équationnelle dans une spécification algébrique axiomatisée par un ensemble d'équations. Une formule équationnelle est une formule universellement quantifiée d'un langage du premier ordre dont les formules atomiques sont des équations simples. Nous proposons de généraliser et d'adapter les méthodes utilisées dans le cas des équations simples pour prouver la validité des formules équationnelles. Ainsi, dans le cas de la validité inductive nous avons utilisé l'induction structurelle basée sur la récurrence classique. Nous avons proposé une méthode pour la génération automatique des schémas d'induction dans certains cas particuliers. Dans le cas de la validité équationnelle nous avons proposé une méthode basée sur la transformation et la décomposition de la formule initiale pour déterminer un ensemble représentatif d'équations simples. La validité équationnelle de ces équations est équivalente à celle de la formule initiale. Un autre mécanisme de raisonnement appelé le chaînage transitif est proposé pour tester la validité des équations contenant des relations d'ordre. L'étude théorique des principes proposés dans cette thèse a abouti à la réalisation du système de preuve pause que nous avons utilisé pour vérifier certaines relations d'asynchronisme entre les composantes qui gèrent la communication dans un système parallèle
Fichier non déposé

Dates et versions

tel-01747712 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01747712 , version 1

Accès intranet

Citer

Noureddine Lazrak. Contribution à la vérification des spécifications algébriques : application à certaines propriétés de programmes parallèles. Autre. Université Henri Poincaré - Nancy 1, 1990. Français. ⟨NNT : 1990NAN10035⟩. ⟨tel-01747712⟩
10 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More