Vérification et mise en œuvre distribuée des programmes unity - Université de Lorraine Accéder directement au contenu
Thèse Année : 1994

Verification and mapping of unity programs into distributed architectures

Vérification et mise en œuvre distribuée des programmes unity

Naïma Brown
  • Fonction : Auteur
  • PersonId : 790681
  • IdRef : 192958046

Résumé

Not available
L'affinement successif de programmes parallèles à partir de spécifications formelles permet de s'assurer de la correction du programme obtenu par rapport a la specification initiale, puisque la transformation est fondée sur la préservation de propriétés telles que celles d'invariance et celles de fatalité. Cependant, les programmes obtenus sont écrits dans une notation abstraite éloignée des langages de programmation parallèles classiques et il convient de développer des techniques de transformation de programmes (ensemble d'actions) en des programmes écrits dans des langages de programmation parallèles (linda, occam). Bien entendu, cela conduit à analyser les techniques possibles de parallélisation de systèmes d'actions ou de distribution de systèmes d'actions. Notre travail de thèse s'appuie sur le formalisme unity de Chandy et Misra pour lequel nous avons construit un outil d'aide à la preuve dans l'outil b et nous avons examiné plusieurs types de transformations de programmes unity en d'autres langages ainsi que des stratégies de répartition. Nous proposons un langage intermédiaire que nous dénommons UCL (unity communication language) qui facilite l'implantation d'unity sur une architecture parallèle, et qui assure la correction formelle de cette implantation vis-à-vis de la spécification initiale. Le langage UCL est ensuite utilisé comme nouveau point de départ de la transformation et permet de produire soit un programme Clinda, soit un programme Occam. Cette approche favorise la réutilisation de cette première étape de transformation avant de cibler une architecture particulière
Fichier non déposé

Dates et versions

tel-01754184 , version 1 (30-03-2018)

Identifiants

  • HAL Id : tel-01754184 , version 1

Accès intranet

Citer

Naïma Brown. Vérification et mise en œuvre distribuée des programmes unity. Autre. Université Henri Poincaré - Nancy 1, 1994. Français. ⟨NNT : 1994NAN10384⟩. ⟨tel-01754184⟩
20 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More