Abstract FR:

Les travaux presentes dans ce memoire portent sur la specification formelle et l'analyse des mecanismes commitment concurrency recovery (ccr) et transaction processing (tp) de la couche application du modele osi de l'iso pour les reseaux d'ordinateurs. Ces mecanismes permettent la realisation d'actions atomiques sur des liaisons bipoints (ccr) et dans un contexte arborescent (tp). Deux techniques complementaires de description formelle sont utilisees: le modele reseaux de petri etiquete (rpte) et le langage estelle. La modelisation de la fonction ccr au moyen du modele rpte a montre en particulier, la necessite, d'une part, de specifier une phase dite d'initialisation de la relation ccr (distribution dynamique des roles superieur et subordonne) et, d'autre part, de definir une nouvelle primitive de service. La specification au moyen du langage estelle d'une architecture transactionnelle a montre, en particulier, l'interet de ce langage pour la specification d'une architecture complexe (comportant cinq niveaux de fonctionnalites du modele osi de l'iso: presentation - ccr ase - tp ase - sacf-macf)